1 /-
2 Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Zhouhang Zhou
5 -/
6
7 import measure_theory.simple_func_dense
src └──────────────────────────────┘
8 import analysis.normed_space.bounded_linear_maps
src └───────────────────────────────────────┘
9
10 /-!
11 # Bochner integral
12
13 The Bochner integral extends the definition of the Lebesgue integral to functions that map from a
14 measure space into a Banach space (complete normed vector space). It is constructed here by
15 extending the integral on simple functions.
16
17 ## Main definitions
18
19 The Bochner integral is defined following these steps:
20
21 1. Define the integral on simple functions of the type `simple_func α β` (notation : `α →ₛ β`)
22 where `β` is a real normed space.
23
24 (See `simple_func.bintegral` and section `bintegral` for details. Also see `simple_func.integral`
25 for the integral on simple functions of the type `simple_func α ennreal`.)
26
27 2. Use `simple_func α β` to cut out the simple functions from L1 functions, and define integral
28 on these. The type of simple functions in L1 space is written as `α →₁ₛ β`.
29
30 3. Show that the embedding of `α →₁ₛ β` into L1 is a dense and uniform one.
31
32 4. Show that the integral defined on `α →₁ₛ β` is a continuous linear map.
33
34 5. Define the Bochner integral on L1 functions by extending the integral on integrable simple
35 functions `α →₁ₛ β` using `continuous_linear_map.extend`. Define the Bochner integral on functions
36 as the Bochner integral of its equivalence class in L1 space.
37
38 ## Main statements
39
40 1. Basic properties of the Bochner integral on functions of type `α → β`, where `α` is a measure
41 space and `β` is a real normed space.
42
43 * `integral_zero` : `∫ 0 = 0`
44 * `integral_add` : `∫ f + g = ∫ f + ∫ g`
45 * `integral_neg` : `∫ -f = - ∫ f`
46 * `integral_sub` : `∫ f - g = ∫ f - ∫ g`
47 * `integral_smul` : `∫ r • f = r • ∫ f`
48 * `integral_congr_ae` : `∀ₘ a, f a = g a → ∫ f = ∫ g`
49 * `norm_integral_le_integral_norm` : `∥∫ f∥ ≤ ∫ ∥f∥`
50
51 2. Basic properties of the Bochner integral on functions of type `α → ℝ`, where `α` is a measure
52 space.
53
54 * `integral_nonneg_of_nonneg_ae` : `∀ₘ a, 0 ≤ f a → 0 ≤ ∫ f`
55 * `integral_nonpos_of_nonpos_ae` : `∀ₘ a, f a ≤ 0 → ∫ f ≤ 0`
56 * `integral_le_integral_of_le_ae` : `∀ₘ a, f a ≤ g a → ∫ f ≤ ∫ g`
57
58 3. Propositions connecting the Bochner integral with the integral on `ennreal`-valued functions,
59 which is called `lintegral` and has the notation `∫⁻`.
60
61 * `integral_eq_lintegral_max_sub_lintegral_min` : `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, where `f⁺` is the positive
62 part of `f` and `f⁻` is the negative part of `f`.
63 * `integral_eq_lintegral_of_nonneg_ae` : `∀ₘ a, 0 ≤ f a → ∫ f = ∫⁻ f`
64
65 4. `tendsto_integral_of_dominated_convergence` : the Lebesgue dominated convergence theorem
66
67 ## Notes
68
69 Some tips on how to prove a proposition if the API for the Bochner integral is not enough so that
70 you need to unfold the definition of the Bochner integral and go back to simple functions.
71
72 See `integral_eq_lintegral_max_sub_lintegral_min` for a complicated example, which proves that
73 `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, with the first integral sign being the Bochner integral of a real-valued
74 function f : α → ℝ, and second and third integral sign being the integral on ennreal-valued
75 functions (called `lintegral`). The proof of `integral_eq_lintegral_max_sub_lintegral_min` is
76 scattered in sections with the name `pos_part`.
77
78 Here are the usual steps of proving that a property `p`, say `∫ f = ∫⁻ f⁺ - ∫⁻ f⁻`, holds for all
79 functions :
80
81 1. First go to the `L¹` space.
82
83 For example, if you see `ennreal.to_real (∫⁻ a, ennreal.of_real $ ∥f a∥)`, that is the norm of `f` in
84 `L¹` space. Rewrite using `l1.norm_of_fun_eq_lintegral_norm`.
85
86 2. Show that the set `{f ∈ L¹ | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}` is closed in `L¹` using `is_closed_eq`.
87
88 3. Show that the property holds for all simple functions `s` in `L¹` space.
89
90 Typically, you need to convert various notions to their `simple_func` counterpart, using lemmas like
91 `l1.integral_coe_eq_integral`.
92
93 4. Since simple functions are dense in `L¹`,
94 ```
95 univ = closure {s simple}
96 = closure {s simple | ∫ s = ∫⁻ s⁺ - ∫⁻ s⁻} : the property holds for all simple functions
97 ⊆ closure {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻}
98 = {f | ∫ f = ∫⁻ f⁺ - ∫⁻ f⁻} : closure of a closed set is itself
99 ```
100 Use `is_closed_property` or `dense_range.induction_on` for this argument.
101
102 ## Notations
103
104 * `α →ₛ β` : simple functions (defined in `measure_theory/integration`)
105 * `α →₁ β` : functions in L1 space, i.e., equivalence classes of integrable functions (defined in
106 `measure_theory/l1_space`)
107 * `α →₁ₛ β` : simple functions in L1 space, i.e., equivalence classes of integrable simple functions
108
109 Note : `ₛ` is typed using `\_s`. Sometimes it shows as a box if font is missing.
110
111 ## Tags
112
113 Bochner integral, simple function, function space, Lebesgue dominated convergence theorem
114
115 -/
116
117 noncomputable theory
118 open_locale classical topological_space
119
120 set_option class.instance_max_depth 100
doc └──────────────────────┘
121
122 -- Typeclass inference has difficulty finding `has_scalar ℝ β` where `β` is a `normed_space` on `ℝ`
123 local attribute [instance, priority 10000]
124 mul_action.to_has_scalar distrib_mul_action.to_mul_action add_comm_group.to_add_comm_monoid
id └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
src └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
typ └──────────────────────┘ └──────────────────────────────┘ └───────────────────────────────┘
125 normed_group.to_add_comm_group normed_space.to_module
id └────────────────────────────┘ └────────────────────┘
src └────────────────────────────┘ └────────────────────┘
typ └────────────────────────────┘ └────────────────────┘
126 module.to_semimodule
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
127
128 namespace measure_theory
129
130 universes u v w
131 variables {α : Type u} [measurable_space α] {β : Type v} [decidable_linear_order β] [has_zero β]
id └──────────────┘ └────────────────────┘ └──────┘
src └──────────────┘ └────────────────────┘ └──────┘
typ └──────────────┘ └────────────────────┘ └──────┘
132
133 local infixr ` →ₛ `:25 := simple_func
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
134
135 namespace simple_func
136
137 section pos_part
138
139 /-- Positive part of a simple function. -/
140 def pos_part (f : α →ₛ β) : α →ₛ β := f.map (λb, max b 0)
id ┴ └┘ ┴ ┴ └┘ ┴ ┴└──┘ ┴ └─┘ ┴
src └┘ └┘ └──┘ └─┘
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴└──┘ ┴ └─┘ ┴
doc └┘ └┘ └──┘
141
142 /-- Negative part of a simple function. -/
143 def neg_part [has_neg β] (f : α →ₛ β) : α →ₛ β := pos_part (-f)
id └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────┘ ┴┴
src └─────┘ └┘ └┘ └──────┘ ┴
typ └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────┘ ┴┴
doc └┘ └┘ └──────┘
144
145 lemma pos_part_map_norm (f : α →ₛ ℝ) : (pos_part f).map norm = pos_part f :=
id ┴ └┘ ┴ └──────┘ ┴ └─┘ └──┘ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ └─┘ └──┘ ┴ └──────┘
typ ┴ └┘ ┴ └──────┘ ┴ └─┘ └──┘ ┴ └──────┘ ┴
doc └┘ └──────┘ └─┘ └──────┘
146 begin
st └─────
147 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
148 rw [map_apply, real.norm_eq_abs, abs_of_nonneg],
id └───────┘ └──────────────┘ └───────────┘
src └──┘└───────┘└┘└──────────────┘└┘└───────────┘┴
typ └──┘└───────┘└┘└──────────────┘└┘└───────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────┘└────────────────┘└─────────────┘└──
149 rw [pos_part, map_apply],
id └──────┘ └───────┘
src └──┘└──────┘└┘└───────┘┴
typ └──┘└──────┘└┘└───────┘┴
doc └──┘└──────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────┘└─────────┘└──
150 exact le_max_right _ _
id └──────────┘
src └────┘└──────────┘└───┘
typ └────┘└──────────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ────────────────────────┘
151 end
st └─┘
152
153 lemma neg_part_map_norm (f : α →ₛ ℝ) : (neg_part f).map norm = neg_part f :=
id ┴ └┘ ┴ └──────┘ ┴ └─┘ └──┘ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ └─┘ └──┘ ┴ └──────┘
typ ┴ └┘ ┴ └──────┘ ┴ └─┘ └──┘ ┴ └──────┘ ┴
doc └┘ └──────┘ └─┘ └──────┘
154 by { rw neg_part, exact pos_part_map_norm _ }
id └──────┘ └───────────────┘
src └─┘└──────┘ └────┘└───────────────┘└─┘
typ └─┘└──────┘ └────┘└───────────────┘└─┘
doc └─┘└──────┘ └────┘ └─┘
txt └─┘ └────┘ └─┘
par └─┘ └────┘ └─┘
pid ┴ ┴ └┘┴
st └────────────┘└──────────────────────────┘└┘
155
156 lemma pos_part_sub_neg_part (f : α →ₛ ℝ) : f.pos_part - f.neg_part = f :=
id ┴ └┘ ┴ ┴└───────┘ ┴ ┴└───────┘ ┴ ┴
src └┘ ┴ └───────┘ ┴ └───────┘ ┴
typ ┴ └┘ ┴ ┴└───────┘ ┴ ┴└───────┘ ┴ ┴
doc └┘ └───────┘ └───────┘
157 begin
st └─────
158 simp only [pos_part, neg_part],
id └──────┘ └──────┘
src └─────────┘└──────┘└┘└──────┘┴
typ └─────────┘└──────┘└┘└──────┘┴
doc └─────────┘└──────┘└┘└──────┘┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───────────────────────────────┘└─
159 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
160 exact max_zero_sub_eq_self (f a)
id └──────────────────┘ ┴ ┴
src └────┘└──────────────────┘┴ ┴ └┘
typ └────┘└──────────────────┘┴ ┴┴┴└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ──────────────────────────────────┘
161 end
st └─┘
162
163 end pos_part
164
165 end simple_func
166
167 end measure_theory
168
169 namespace measure_theory
170 open set lattice filter topological_space ennreal emetric
171
172 universes u v w
173 variables {α : Type u} [measure_space α] {β : Type v} {γ : Type w}
id ┴ └───────────┘
src └───────────┘
typ ┴ └───────────┘
doc └───────────┘
174
175 local infixr ` →ₛ `:25 := simple_func
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
176
177 namespace simple_func
178
179 section bintegral
180 /-!
181 ### The Bochner integral of simple functions
182
183 Define the Bochner integral of simple functions of the type `α →ₛ β` where `β` is a normed group,
184 and prove basic property of this integral.
185 -/
186 open finset
187
188 variables [normed_group β] [normed_group γ]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
189
190 lemma integrable_iff_integral_lt_top {f : α →ₛ β} :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
191 integrable f ↔ integral (f.map (coe ∘ nnnorm)) < ⊤ :=
id └────────┘ ┴ ┴ └──────┘ ┴└──┘ └─┘ ┴ └────┘ ┴ ┴
src └────────┘ ┴ └──────┘ └──┘ └─┘ ┴ └────┘ ┴ ┴
typ └────────┘ ┴ ┴ └──────┘ ┴└──┘ └─┘ ┴ └────┘ ┴ ┴
doc └────────┘ └──────┘ └──┘ └────┘
192 by { rw [integrable, ← lintegral_eq_integral, lintegral_map] }
id └────────┘ └───────────────────┘ └───────────┘
src └──┘└────────┘└──┘└───────────────────┘└┘└───────────┘└┘
typ └──┘└────────┘└──┘└───────────────────┘└┘└───────────┘└┘
doc └──┘└────────┘└──┘ └┘ └┘
txt └──┘ └──┘ └┘ └┘
par └──┘ └──┘ └┘ └┘
pid └┘ └──┘ └┘ ┴┴
st └───────────────┘└───────────────────────┘└─────────────┘┴┴└┘
193
194 lemma fin_vol_supp_of_integrable {f : α →ₛ β} (hf : integrable f) : f.fin_vol_supp :=
id ┴ └┘ ┴ └────────┘ ┴ ┴└───────────┘
src └┘ └────────┘ └───────────┘
typ ┴ └┘ ┴ └────────┘ ┴ ┴└───────────┘
doc └┘ └────────┘
195 begin
st └─────
196 rw [integrable_iff_integral_lt_top] at hf,
id └────────────────────────────┘
src └──┘└────────────────────────────┘└─────┘
typ └──┘└────────────────────────────┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid └┘ ┴└────┘
st ───────────────────────────────────┘┴└────┘└─
197 have hf := fin_vol_supp_of_integral_lt_top hf,
id └─────────────────────────────┘ └┘
src └─────────┘└─────────────────────────────┘┴
typ └─────────┘└─────────────────────────────┘┴└┘
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └─────┘┴└─┘ ┴
st ──────────────────────────────────────────────┘└─
198 refine fin_vol_supp_of_fin_vol_supp_map f hf _,
id └──────────────────────────────┘ ┴ └┘
src └─────┘└──────────────────────────────┘┴ ┴ └┘
typ └─────┘└──────────────────────────────┘┴┴┴└┘└┘
doc └─────┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────┘└─
199 assume b, simp [nnnorm_eq_zero]
id └────────────┘
src └──────┘ └────┘└────────────┘└┘
typ └──────┘ └────┘└────────────┘└┘
doc └──────┘ └────┘ └┘
txt └──────┘ └────┘ └┘
par └──────┘ └────┘ └┘
pid └──────┘ ┴┴ ┴┴
st ─────────┘└──────────────────────┘
200 end
st └─┘
201
202 lemma integrable_of_fin_vol_supp {f : α →ₛ β} (h : f.fin_vol_supp) : integrable f :=
id ┴ └┘ ┴ ┴└───────────┘ └────────┘ ┴
src └┘ └───────────┘ └────────┘
typ ┴ └┘ ┴ ┴└───────────┘ └────────┘ ┴
doc └┘ └────────┘
203 by { rw [integrable_iff_integral_lt_top], exact integral_map_coe_lt_top h nnnorm_zero }
id └────────────────────────────┘ └─────────────────────┘ ┴ └─────────┘
src └──┘└────────────────────────────┘┴ └────┘└─────────────────────┘┴ ┴└─────────┘┴
typ └──┘└────────────────────────────┘┴ └────┘└─────────────────────┘┴┴┴└─────────┘┴
doc └──┘ ┴ └────┘└─────────────────────┘┴ ┴ ┴
txt └──┘ ┴ └────┘ ┴ ┴ ┴
par └──┘ ┴ └────┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────────┘└─────────────────────────────────────────────┘└┘
204
205 /-- For simple functions with a `normed_group` as codomain, being integrable is the same as having
206 finite volume support. -/
207 lemma integrable_iff_fin_vol_supp (f : α →ₛ β) : integrable f ↔ f.fin_vol_supp :=
id ┴ └┘ ┴ └────────┘ ┴ ┴ ┴└───────────┘
src └┘ └────────┘ ┴ └───────────┘
typ ┴ └┘ ┴ └────────┘ ┴ ┴ ┴└───────────┘
doc └┘ └────────┘
208 iff.intro fin_vol_supp_of_integrable integrable_of_fin_vol_supp
id └───────┘ └────────────────────────┘ └────────────────────────┘
src └───────┘ └────────────────────────┘ └────────────────────────┘
typ └───────┘ └────────────────────────┘ └────────────────────────┘
209
210 lemma integrable_pair {f : α →ₛ β} {g : α →ₛ γ} (hf : integrable f) (hg : integrable g) :
id ┴ └┘ ┴ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
src └┘ └┘ └────────┘ └────────┘
typ ┴ └┘ ┴ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └┘ └┘ └────────┘ └────────┘
211 integrable (pair f g) :=
id └────────┘ └──┘ ┴ ┴
src └────────┘ └──┘
typ └────────┘ └──┘ ┴ ┴
doc └────────┘ └──┘
212 by { rw integrable_iff_fin_vol_supp at *, apply fin_vol_supp_pair; assumption }
id └─────────────────────────┘ └───────────────┘
src └─┘└─────────────────────────┘└───┘ └────┘└───────────────┘ └─────────┘
typ └─┘└─────────────────────────┘└───┘ └────┘└───────────────┘ └─────────┘
doc └─┘└─────────────────────────┘└───┘ └────┘ └─────────┘
txt └─┘ └───┘ └────┘ └─────────┘
par └─┘ └───┘ └────┘ └─────────┘
pid ┴ └───┘ ┴ ┴
st └────────────────────────────────────┘└────────────────────────────────────┘└┘
213
214 variables [normed_space ℝ γ]
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘
215
216 /-- Bochner integral of simple functions whose codomain is a real `normed_space`.
217 The name `simple_func.integral` has been taken in the file `integration.lean`, which calculates
218 the integral of a simple function with type `α → ennreal`.
219 The name `bintegral` stands for Bochner integral. -/
220 def bintegral [normed_space ℝ β] (f : α →ₛ β) : β :=
id └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴
src └──────────┘ ┴ └┘
typ └──────────┘ ┴ ┴ ┴ └┘ ┴ ┴
doc └──────────┘ └┘
221 f.range.sum (λ x, (ennreal.to_real (volume (f ⁻¹' {x}))) • x)
id ┴└────┘└──┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴
src └────┘└──┘ └─────────────┘ └────┘ └─┘ ┴ ┴
typ ┴└────┘└──┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴
doc └────┘ └─────────────┘ └─┘
222
223 /-- Calculate the integral of `g ∘ f : α →ₛ γ`, where `f` is an integrable function from `α` to `β`
224 and `g` is a function from `β` to `γ`. We require `g 0 = 0` so that `g ∘ f` is integrable. -/
225 lemma map_bintegral (f : α →ₛ β) (g : β → γ) (hf : integrable f) (hg : g 0 = 0) :
id ┴ └┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
src └┘ └────────┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴
doc └┘ └────────┘
226 (f.map g).bintegral = f.range.sum (λ x, (ennreal.to_real (volume (f ⁻¹' {x}))) • (g x)) :=
id ┴└──┘ ┴ └───────┘ ┴ ┴└────┘└──┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴
src └──┘ └───────┘ ┴ └────┘└──┘ └─────────────┘ └────┘ └─┘ ┴ ┴
typ ┴└──┘ ┴ └───────┘ ┴ ┴└────┘└──┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴
doc └──┘ └───────┘ └────┘ └─────────────┘ └─┘
227 begin
st └─────
228 /- Just a complicated calculation with `finset.sum`. Real work is done by
st ────────────────────────────────────────────────────────────────────────────
229 `map_preimage_singleton`, `simple_func.volume_bUnion_preimage` and `ennreal.to_real_sum` -/
st ──────────────────────────────────────────────────────────────────────────────────────────────────
230 rw integrable_iff_fin_vol_supp at hf,
id └─────────────────────────┘
src └─┘└─────────────────────────┘└────┘
typ └─┘└─────────────────────────┘└────┘
doc └─┘└─────────────────────────┘└────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ─────────────────────────────────────┘└─
231 simp only [bintegral, range_map],
id └───────┘ └───────┘
src └─────────┘└───────┘└┘└───────┘┴
typ └─────────┘└───────┘└┘└───────┘┴
doc └─────────┘└───────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ─────────────────────────────────┘└─
232 refine finset.sum_image' _ (assume b hb, _),
id └───────────────┘
src └─────┘└───────────────┘└─┘ └───────┘
typ └─────┘└───────────────┘└─┘ └───────┘
doc └─────┘ └─┘ └───────┘
txt └─────┘ └─┘ └───────┘
par └─────┘ └─┘ └───────┘
pid ┴ └─┘ └───────┘
st ────────────────────────────────────────────┘└─
233 rcases mem_range.1 hb with ⟨a, rfl⟩,
id └───────┘ └┘
src └─────┘└───────┘└─┘ └────────────┘
typ └─────┘└───────┘└─┘└┘└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ────────────────────────────────────┘└─
234 let s' := f.range.filter (λb, g b = g (f a)),
id └────────────┘ ┴ ┴ ┴ ┴
src └────────┘└────────────┘┴ └─┘ ┴ ┴┴┴ ┴ ┴ └┘
typ └────────┘└────────────┘┴ └─┘ ┴ ┴┴┴┴┴ ┴┴┴└┘
doc └────────┘└────────────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
txt └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
par └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
pid └────┘┴└─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────┘└─
235 calc (ennreal.to_real (volume ((f.map g) ⁻¹' {g (f a)}))) • (g (f a)) =
id └──┘ └───┘ └─┘ ┴ ┴
src └──┘ └───┘ └─┘ ┴ ┴
typ └──┘ └───┘ └─┘ ┴ ┴
doc └──┘ └───┘ └─┘
st ──────────────────────────────────────────────────────────────────────────
236 (ennreal.to_real (volume (⋃b∈s', f ⁻¹' {b}))) • (g (f a)) : by rw map_preimage_singleton
id └─────────────┘ └────┘ ┴┴ └┘┴ ┴ ┴ ┴ └────────────────────┘
src └─────────────┘ └────┘ ┴ ┴ └─┘└────────────────────┘└
typ └─────────────┘ └────┘ ┴┴ └┘┴ ┴ ┴ ┴ └─┘└────────────────────┘└
doc └─────────────┘ ┴ ┴ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ───────────────────────────────────────────────────────────────────┘└──────────────────────────
237 ... = (ennreal.to_real (s'.sum (λb, volume (f ⁻¹' {b})))) • (g (f a)) :
id └────┘ ┴
src ─┘ └────┘
typ ─┘ └────┘ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└───────────────────────────────────────────────────────────────────────
238 by rw volume_bUnion_preimage
id └────────────────────┘
src └─┘└────────────────────┘└
typ └─┘└────────────────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ─────┘└──────────────────────────
239 ... = (s'.sum (λb, ennreal.to_real (volume (f ⁻¹' {b})))) • (g (f a)) :
id ┴
src ─┘
typ ─┘ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└───────────────────────────────────────────────────────────────────────
240 begin
st ─┘└─────
241 by_cases h : g (f a) = 0,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴ └┘ └┘
typ └───────┘ └─┘┴┴ ┴┴┴└┘ └┘
doc └───────┘ └─┘ ┴ ┴ └┘ └┘
txt └───────┘ └─┘ ┴ ┴ └┘ └┘
par └───────┘ └─┘ ┴ ┴ └┘ └┘
pid ┴ └─┘ ┴ ┴ └┘ ┴┴
st ───────────────────────────┘└─
242 { rw [h, smul_zero, smul_zero] },
id ┴ └───────┘ └───────┘
src └──┘ └┘└───────┘└┘└───────┘└┘
typ └──┘┴└┘└───────┘└┘└───────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ─────┘└───┘└─────────┘└─────────┘┴┴└┘└
243 { rw ennreal.to_real_sum,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘└─────────────────┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────┘└─
244 simp only [mem_filter],
id └────────┘
src └─────────┘└────────┘┴
typ └─────────┘└────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ───────────────────────────┘└─
245 rintros b ⟨_, hb⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ──────────────────────┘└─
246 have : b ≠ 0, { assume hb', rw [← hb, hb'] at h, contradiction },
id ┴ ┴ └┘ └─┘
src └─────┘ ┴┴└┘ └────────┘ └────┘ └┘ └────┘ └────────────┘
typ └─────┘┴┴┴└┘ └────────┘ └────┘└┘└┘└─┘└────┘ └────────────┘
doc └─────┘ ┴ └┘ └────────┘ └────┘ └┘ └────┘ └────────────┘
txt └─────┘ ┴ └┘ └────────┘ └────┘ └┘ └────┘ └────────────┘
par └─────┘ ┴ └┘ └────────┘ └────┘ └┘ └────┘ └────────────┘
pid └───┘└┘ ┴ ┴┴ └────────┘ └──┘ └┘ ┴└───┘ ┴
st ─────────────────┘└──┘└────────┘└────────┘└───┘┴└───┘└──────────────┘└┘└
247 apply hf,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
248 assumption }
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid ┴
st ────────────────┘└─
249 end
st ────┘└
250 ... = s'.sum (λb, (ennreal.to_real (volume (f ⁻¹' {b}))) • (g (f a))) : finset.sum_smul
id ┴ └─────────────┘
src └─────────────┘
typ ┴ └─────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────────
251 ... = s'.sum (λb, (ennreal.to_real (volume (f ⁻¹' {b}))) • (g b)) :
id ┴
typ ┴
st ──────────────────────────────────────────────────────────────────────
252 finset.sum_congr rfl $ by { assume x, simp only [mem_filter], rintro ⟨_, h⟩, rw h }
id └──────────────┘ └─┘ └────────┘ ┴
src └──────────────┘ └─┘ └──────┘ └─────────┘└────────┘┴ └───────────┘ └─┘ ┴
typ └──────────────┘ └─┘ └──────┘ └─────────┘└────────┘┴ └───────────┘ └─┘┴┴
doc └──────┘ └─────────┘ ┴ └───────────┘ └─┘ ┴
txt └──────┘ └─────────┘ ┴ └───────────┘ └─┘ ┴
par └──────┘ └─────────┘ ┴ └───────────┘ └─┘ ┴
pid └──────┘ ┴└──┘└┘ ┴ └─────┘ ┴ ┴
st ────────────────────────────┘└─────────┘└──────────────────────┘└─────────────┘└─────┘└─
253 end
st ──┘
254
255 /-- `simple_func.bintegral` and `simple_func.integral` agree when the integrand has type
256 `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion.
257 See `bintegral_eq_integral'` for a simpler version. -/
258 lemma bintegral_eq_integral {f : α →ₛ β} {g : β → ennreal} (hf : integrable f) (hg0 : g 0 = 0)
id ┴ └┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ ┴
src └┘ └─────┘ └────────┘ ┴
typ ┴ └┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ ┴
doc └┘ └─────┘ └────────┘
259 (hgt : ∀b, g b < ⊤):
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
260 (f.map (ennreal.to_real ∘ g)).bintegral = ennreal.to_real (f.map g).integral :=
id ┴└──┘ └─────────────┘ ┴ ┴ └───────┘ ┴ └─────────────┘ ┴└──┘ ┴ └──────┘
src └──┘ └─────────────┘ ┴ └───────┘ ┴ └─────────────┘ └──┘ └──────┘
typ ┴└──┘ └─────────────┘ ┴ ┴ └───────┘ ┴ └─────────────┘ ┴└──┘ ┴ └──────┘
doc └──┘ └─────────────┘ └───────┘ └─────────────┘ └──┘ └──────┘
261 begin
st └─────
262 have hf' : f.fin_vol_supp, { rwa integrable_iff_fin_vol_supp at hf },
id └────────────┘ └─────────────────────────┘
src └─────────┘└────────────┘ └──┘└─────────────────────────┘└─────┘
typ └─────────┘└────────────┘ └──┘└─────────────────────────┘└─────┘
doc └─────────┘ └──┘└─────────────────────────┘└─────┘
txt └─────────┘ └──┘ └─────┘
par └─────────┘ └──┘ └─────┘
pid └──────┘└─┘ ┴ └────┘┴
st ──────────────────────────┘└──┘└────────────────────────────────────┘└┘└
263 rw [map_bintegral f _ hf, map_integral, ennreal.to_real_sum],
id └───────────┘ ┴ └┘ └──────────┘ └─────────────────┘
src └──┘└───────────┘┴ └─┘ └┘└──────────┘└┘└─────────────────┘┴
typ └──┘└───────────┘┴┴└─┘└┘└┘└──────────┘└┘└─────────────────┘┴
doc └──┘└───────────┘┴ └─┘ └┘└──────────┘└┘└─────────────────┘┴
txt └──┘ ┴ └─┘ └┘ └┘ ┴
par └──┘ ┴ └─┘ └┘ └┘ ┴
pid └┘ ┴ └─┘ └┘ └┘ ┴
st ─────────────────────────┘└────────────┘└───────────────────┘└──
264 { refine finset.sum_congr rfl (λb hb, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └──────┘
typ └─────┘└──────────────┘┴└─┘┴ └──────┘
doc └─────┘ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ───┘└────────────────────────────────────┘└─
265 rw [smul_eq_mul],
id └─────────┘
src └──┘└─────────┘┴
typ └──┘└─────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────────┘└──
266 rw [to_real_mul_to_real, mul_comm] },
id └─────────────────┘ └──────┘
src └──┘└─────────────────┘└┘└──────┘└┘
typ └──┘└─────────────────┘└┘└──────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────────────────────────┘└────────┘┴┴└┘└
267 { assume a ha,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
268 by_cases a0 : a = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ──────────────────────┘└─
269 { rw [a0, hg0, zero_mul], exact with_top.zero_lt_top },
id └┘ └─┘ └──────┘ └──────────────────┘
src └──┘ └┘ └┘└──────┘┴ └────┘└──────────────────┘┴
typ └──┘└┘└┘└─┘└┘└──────┘┴ └────┘└──────────────────┘┴
doc └──┘ └┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ └┘ ┴ ┴ ┴
st ─────┘└────┘└───┘└────────┘└────────────────────────────┘└┘└
270 apply mul_lt_top (hgt a) (hf' _ a0) },
id └────────┘ └─┘ ┴ └─┘ └┘
src └────┘└────────┘┴ ┴ └┘ └─┘ └┘
typ └────┘└────────┘┴ └─┘┴┴└┘ └─┘└─┘└┘└┘
doc └────┘ ┴ ┴ └┘ └─┘ └┘
txt └────┘ ┴ ┴ └┘ └─┘ └┘
par └────┘ ┴ ┴ └┘ └─┘ └┘
pid ┴ ┴ ┴ └┘ └─┘ ┴┴
st ───────────────────────────────────────┘└┘└
271 { simp [hg0] }
id └─┘
src └────┘ └┘
typ └────┘└─┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ──────────────┘└─
272 end
st ──┘
273
274 /-- `simple_func.bintegral` and `lintegral : (α → ennreal) → ennreal` are the same when the
275 integrand has type `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some
276 form of coercion.
277 See `bintegral_eq_lintegral'` for a simpler version. -/
278 lemma bintegral_eq_lintegral (f : α →ₛ β) (g : β → ennreal) (hf : integrable f) (hg0 : g 0 = 0)
id ┴ └┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ ┴
src └┘ └─────┘ └────────┘ ┴
typ ┴ └┘ ┴ ┴ └─────┘ └────────┘ ┴ ┴ ┴
doc └┘ └─────┘ └────────┘
279 (hgt : ∀b, g b < ⊤):
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
280 (f.map (ennreal.to_real ∘ g)).bintegral = ennreal.to_real (∫⁻ a, g (f a)) :=
id ┴└──┘ └─────────────┘ ┴ ┴ └───────┘ ┴ └─────────────┘ └┘ ┴┴ ┴ ┴ ┴
src └──┘ └─────────────┘ ┴ └───────┘ ┴ └─────────────┘ └┘ ┴
typ ┴└──┘ └─────────────┘ ┴ ┴ └───────┘ ┴ └─────────────┘ └┘ ┴┴ ┴ ┴ ┴
doc └──┘ └─────────────┘ └───────┘ └─────────────┘ └┘ ┴
281 by { rw [bintegral_eq_integral hf hg0 hgt, ← lintegral_eq_integral], refl }
id └───────────────────┘ └┘ └─┘ └─┘ └───────────────────┘
src └──┘└───────────────────┘┴ ┴ ┴ └──┘└───────────────────┘┴ └───┘
typ └──┘└───────────────────┘┴└┘┴└─┘┴└─┘└──┘└───────────────────┘┴ └───┘
doc └──┘└───────────────────┘┴ ┴ ┴ └──┘ ┴ └───┘
txt └──┘ ┴ ┴ ┴ └──┘ ┴ └───┘
par └──┘ ┴ ┴ ┴ └──┘ ┴ └───┘
pid └┘ ┴ ┴ ┴ └──┘ ┴ ┴
st └─────────────────────────────────────┘└───────────────────────┘└──────┘└┘
282
283 variables [normed_space ℝ β]
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘
284
285 lemma bintegral_congr {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) (h : ∀ₘ a, f a = g a):
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ └────────┘ └────────┘ └┘ ┴ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └────────┘ └────────┘ └┘ ┴
286 bintegral f = bintegral g :=
id └───────┘ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ └───────┘ ┴
doc └───────┘ └───────┘
287 show ((pair f g).map prod.fst).bintegral = ((pair f g).map prod.snd).bintegral, from
id └──┘ ┴ ┴ └─┘ └──────┘ └───────┘ ┴ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘
src └──┘ └─┘ └──────┘ └───────┘ ┴ └──┘ └─┘ └──────┘ └───────┘
typ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘ ┴ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘
doc └──┘ └─┘ └───────┘ └──┘ └─┘ └───────┘
288 begin
st └─────
289 have inte := integrable_pair hf hg,
id └─────────────┘ └┘ └┘
src └───────────┘└─────────────┘┴ ┴
typ └───────────┘└─────────────┘┴└┘┴└┘
doc └───────────┘ ┴ ┴
txt └───────────┘ ┴ ┴
par └───────────┘ ┴ ┴
pid └───────┘┴└─┘ ┴ ┴
st ───────────────────────────────────┘└─
290 rw [map_bintegral (pair f g) _ inte prod.fst_zero, map_bintegral (pair f g) _ inte prod.snd_zero],
id └───────────┘ └──┘ ┴ ┴ └──┘ └───────────┘ └───────────┘ └──┘ ┴ ┴ └──┘ └───────────┘
src └──┘└───────────┘┴ └──┘┴ ┴ └──┘ ┴└───────────┘└┘└───────────┘┴ └──┘┴ ┴ └──┘ ┴└───────────┘┴
typ └──┘└───────────┘┴ └──┘┴┴┴┴└──┘└──┘┴└───────────┘└┘└───────────┘┴ └──┘┴┴┴┴└──┘└──┘┴└───────────┘┴
doc └──┘└───────────┘┴ └──┘┴ ┴ └──┘ ┴ └┘└───────────┘┴ └──┘┴ ┴ └──┘ ┴ ┴
txt └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
par └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
pid └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────┘└─────────────────────────────────────────────┘└──
291 refine finset.sum_congr rfl (assume p hp, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └───────┘
typ └─────┘└──────────────┘┴└─┘┴ └───────┘
doc └─────┘ ┴ ┴ └───────┘
txt └─────┘ ┴ ┴ └───────┘
par └─────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ─────────────────────────────────────────────┘└─
292 rcases mem_range.1 hp with ⟨a, rfl⟩,
id └───────┘ └┘
src └─────┘└───────┘└─┘ └────────────┘
typ └─────┘└───────┘└─┘└┘└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ────────────────────────────────────┘└─
293 by_cases eq : f a = g a,
id ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴┴ ┴
typ └───────┘ └─┘┴┴ ┴┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
294 { dsimp only [pair_apply], rw eq },
id └────────┘ └┘
src └──────────┘└────────┘┴ └─┘└┘┴
typ └──────────┘└────────┘┴ └─┘└┘┴
doc └──────────┘ ┴ └─┘ ┴
txt └──────────┘ ┴ └─┘ ┴
par └──────────┘ ┴ └─┘ ┴
pid └───┘└┘ ┴ ┴ ┴
st ───┘└─────────────────────┘└──────┘└┘└
295 { have : volume ((pair f g) ⁻¹' {(f a, g a)}) = 0,
id └────┘ └──┘ └─┘ ┴┴┴ ┴ ┴
src └─────┘└────┘┴ └──┘┴ ┴ └┘└─┘┴┴┴ ┴ └┘ ┴ └──┘ └┘
typ └─────┘└────┘┴ └──┘┴ ┴ └┘└─┘┴┴┴┴┴ └┘┴┴┴└──┘ └┘
doc └─────┘ ┴ └──┘┴ ┴ └┘└─┘┴ ┴ └┘ ┴ └──┘ └┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ ┴┴
st ──────────────────────────────────────────────────┘└─
296 { refine volume_mono_null (assume a' ha', _) h,
id └──────────────┘ ┴
src └─────┘└──────────────┘┴ └──────────┘
typ └─────┘└──────────────┘┴ └──────────┘┴
doc └─────┘ ┴ └──────────┘
txt └─────┘ ┴ └──────────┘
par └─────┘ ┴ └──────────┘
pid ┴ ┴ └──────────┘
st ─────┘└──────────────────────────────────────────┘└─
297 simp only [set.mem_preimage, mem_singleton_iff, pair_apply, prod.mk.inj_iff] at ha',
id └──────────────┘ └───────────────┘ └────────┘ └─────────────┘
src └─────────┘└──────────────┘└┘└───────────────┘└┘└────────┘└┘└─────────────┘└──────┘
typ └─────────┘└──────────────┘└┘└───────────────┘└┘└────────┘└┘└─────────────┘└──────┘
doc └─────────┘ └┘ └┘ └┘ └──────┘
txt └─────────┘ └┘ └┘ └┘ └──────┘
par └─────────┘ └┘ └┘ └┘ └──────┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴└────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
298 show f a' ≠ g a',
id ┴ ┴ ┴ └┘
src └───┘ ┴ ┴┴┴ ┴
typ └───┘┴┴ ┴┴┴┴┴└┘
doc └───┘ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴
st ─────────────────────┘└─
299 rwa [ha'.1, ha'.2] },
id └─┘ └─┘
src └───┘ └──┘ └──┘
typ └───┘└─┘└──┘└─┘└──┘
doc └───┘ └──┘ └──┘
txt └───┘ └──┘ └──┘
par └───┘ └──┘ └──┘
pid └┘ └──┘ └─┘┴
st ─────────────┘└─────┘└─┘┴└┘└
300 simp only [this, pair_apply, zero_smul, ennreal.zero_to_real] },
id └──┘ └────────┘ └───────┘ └──────────────────┘
src └─────────┘ └┘└────────┘└┘└───────┘└┘└──────────────────┘└┘
typ └─────────┘└──┘└┘└────────┘└┘└───────┘└┘└──────────────────┘└┘
doc └─────────┘ └┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────┘└──
301 end
st ──┘
302
303 /-- `simple_func.bintegral` and `simple_func.integral` agree when the integrand has type
304 `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion. -/
305 lemma bintegral_eq_integral' {f : α →ₛ ℝ} (hf : integrable f) (h_pos : ∀ₘ a, 0 ≤ f a) :
id ┴ └┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
src └┘ ┴ └────────┘ └┘ ┴ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └┘ └────────┘ └┘ ┴
306 f.bintegral = ennreal.to_real (f.map ennreal.of_real).integral :=
id ┴└────────┘ ┴ └─────────────┘ ┴└──┘ └─────────────┘ └──────┘
src └────────┘ ┴ └─────────────┘ └──┘ └─────────────┘ └──────┘
typ ┴└────────┘ ┴ └─────────────┘ ┴└──┘ └─────────────┘ └──────┘
doc └────────┘ └─────────────┘ └──┘ └─────────────┘ └──────┘
307 begin
st └─────
308 have : ∀ₘ a, f a = (f.map (ennreal.to_real ∘ ennreal.of_real)) a,
id └┘ ┴ ┴ └───┘ └─────────────┘ ┴ └─────────────┘
src └─────┘└┘└┘┴┴ ┴ ┴┴┴ └───┘┴ └─────────────┘┴┴┴└─────────────┘└─┘
typ └─────┘└┘└┘┴┴ ┴ ┴┴┴ └───┘┴ └─────────────┘┴┴┴└─────────────┘└─┘
doc └─────┘└┘└┘┴┴ ┴ ┴ ┴ └───┘┴ └─────────────┘┴ ┴└─────────────┘└─┘
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
st ─────────────────────────────────────────────────────────────────┘└─
309 { filter_upwards [h_pos],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ───┘└────────────────────┘└─
310 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
311 simp only [mem_set_of_eq, map_apply, function.comp_apply],
id └───────────┘ └───────┘ └─────────────────┘
src └─────────┘└───────────┘└┘└───────┘└┘└─────────────────┘┴
typ └─────────┘└───────────┘└┘└───────┘└┘└─────────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────┘└─
312 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
313 exact (ennreal.to_real_of_real h).symm },
id └─────────────────────┘ ┴
src └────┘ └─────────────────────┘┴ └─────┘
typ └────┘ └─────────────────────┘┴┴└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └───┘└┘
st ──────────────────────────────────────────┘└┘└
314 rw ← bintegral_eq_integral hf,
id └───────────────────┘ └┘
src └───┘└───────────────────┘┴
typ └───┘└───────────────────┘┴└┘
doc └───┘└───────────────────┘┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ──────────────────────────────┘└─
315 { refine bintegral_congr hf _ this, exact integrable_of_ae_eq hf this },
id └─────────────┘ └┘ └──┘ └─────────────────┘ └┘ └──┘
src └─────┘└─────────────┘┴ └─┘ └────┘└─────────────────┘┴ ┴ ┴
typ └─────┘└─────────────┘┴└┘└─┘└──┘ └────┘└─────────────────┘┴└┘┴└──┘┴
doc └─────┘ ┴ └─┘ └────┘ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ └────┘ ┴ ┴ ┴
par └─────┘ ┴ └─┘ └────┘ ┴ ┴ ┴
pid ┴ ┴ └─┘ ┴ ┴ ┴ ┴
st ───┘└──────────────────────────────┘└──────────────────────────────────┘└┘└
316 { exact ennreal.of_real_zero },
id └──────────────────┘
src └────┘└──────────────────┘┴
typ └────┘└──────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└─────────────────────────┘└┘└
317 { assume b, rw ennreal.lt_top_iff_ne_top, exact ennreal.of_real_ne_top }
id └───────────────────────┘ └────────────────────┘
src └──────┘ └─┘└───────────────────────┘ └────┘└────────────────────┘└┘
typ └──────┘ └─┘└───────────────────────┘ └────┘└────────────────────┘└┘
doc └──────┘ └─┘ └────┘ └┘
txt └──────┘ └─┘ └────┘ └┘
par └──────┘ └─┘ └────┘ └┘
pid └──────┘ ┴ ┴ └┘
st ───────────┘└────────────────────────────┘└──────────────────────────────┘└─
318 end
st ──┘
319
320 /-- `simple_func.bintegral` and `lintegral : (α → ennreal) → ennreal` agree when the integrand has
321 type `α →ₛ ennreal`. But since `ennreal` is not a `normed_space`, we need some form of coercion. -/
322 lemma bintegral_eq_lintegral' {f : α →ₛ ℝ} (hf : integrable f) (h_pos : ∀ₘ a, 0 ≤ f a) :
id ┴ └┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
src └┘ ┴ └────────┘ └┘ ┴ ┴
typ ┴ └┘ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └┘ └────────┘ └┘ ┴
323 f.bintegral = ennreal.to_real (∫⁻ a, (f.map ennreal.of_real a)) :=
id ┴└────────┘ ┴ └─────────────┘ └┘ ┴┴ ┴└──┘ └─────────────┘ ┴
src └────────┘ ┴ └─────────────┘ └┘ ┴ └──┘ └─────────────┘
typ ┴└────────┘ ┴ └─────────────┘ └┘ ┴┴ ┴└──┘ └─────────────┘ ┴
doc └────────┘ └─────────────┘ └┘ ┴ └──┘ └─────────────┘
324 by rw [bintegral_eq_integral' hf h_pos, ← lintegral_eq_integral]
id └────────────────────┘ └┘ └───┘ └───────────────────┘
src └──┘└────────────────────┘┴ ┴ └──┘└───────────────────┘└─
typ └──┘└────────────────────┘┴└┘┴└───┘└──┘└───────────────────┘└─
doc └──┘└────────────────────┘┴ ┴ └──┘ └─
txt └──┘ ┴ ┴ └──┘ └─
par └──┘ ┴ ┴ └──┘ └─
pid └┘ ┴ ┴ └──┘ ┴└
st └──────────────────────────────────┘└───────────────────────┘┴└
325
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
326 lemma bintegral_add {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) :
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
src └┘ └────────┘ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └┘ └────────┘ └────────┘
327 bintegral (f + g) = bintegral f + bintegral g :=
id └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
doc └───────┘ └───────┘ └───────┘
328 calc bintegral (f + g) = sum (pair f g).range
id └───────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └───┘
src └───────┘ ┴ └─┘ └──┘ └───┘
typ └───────┘ ┴ ┴ ┴ └─┘ └──┘ ┴ ┴ └───┘
doc └───────┘ └──┘ └───┘
329 (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • (x.fst + x.snd)) :
id ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴ ┴└──┘
src └─────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴ ┴└──┘
doc └─────────────┘ └──┘ └─┘
330 begin
st └─────
331 rw [add_eq_map₂, map_bintegral (pair f g)],
id └─────────┘ └───────────┘ └──┘ ┴ ┴
src └──┘└─────────┘└┘└───────────┘┴ └──┘┴ ┴ └┘
typ └──┘└─────────┘└┘└───────────┘┴ └──┘┴┴┴┴└┘
doc └──┘ └┘└───────────┘┴ └──┘┴ ┴ └┘
txt └──┘ └┘ ┴ ┴ ┴ └┘
par └──┘ └┘ ┴ ┴ ┴ └┘
pid └┘ └┘ ┴ ┴ ┴ └┘
st ────────────────┘└────────────────────────┘└──
332 { exact integrable_pair hf hg },
id └─────────────┘ └┘ └┘
src └────┘└─────────────┘┴ ┴ ┴
typ └────┘└─────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───┘└──────────────────────────┘└┘└
333 { simp only [add_zero, prod.fst_zero, prod.snd_zero] }
id └──────┘ └───────────┘ └───────────┘
src └─────────┘└──────┘└┘└───────────┘└┘└───────────┘└┘
typ └─────────┘└──────┘└┘└───────────┘└┘└───────────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st ──────────────────────────────────────────────────────┘└─
334 end
st ──┘
335 ... = sum (pair f g).range
id └─┘ └──┘ ┴ ┴ └───┘
src └─┘ └──┘ └───┘
typ └─┘ └──┘ ┴ ┴ └───┘
doc └──┘ └───┘
336 (λx, ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst +
id ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴
src └─────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └──┘ ┴
typ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴
doc └─────────────┘ └──┘ └─┘
337 ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
id └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘
src └─────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └──┘
typ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘
doc └─────────────┘ └──┘ └─┘
338 finset.sum_congr rfl $ assume a ha, smul_add _ _ _
id └──────────────┘ └─┘ ┴ └┘ └──────┘
src └──────────────┘ └─┘ └──────┘
typ └──────────────┘ └─┘ ┴ └┘ └──────┘
339 ... = sum (simple_func.range (pair f g))
id └─┘ └───────────────┘ └──┘ ┴ ┴
src └─┘ └───────────────┘ └──┘
typ └─┘ └───────────────┘ └──┘ ┴ ┴
doc └───────────────┘ └──┘
340 (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.fst) +
id ┴ ┴ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴
src ┴ └─────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘ ┴
doc └─────────────┘ └──┘ └─┘
341 sum (simple_func.range (pair f g))
id └─┘ └───────────────┘ └──┘ ┴ ┴
src └─┘ └───────────────┘ └──┘
typ └─┘ └───────────────┘ └──┘ ┴ ┴
doc └───────────────┘ └──┘
342 (λ (x : β × β), ennreal.to_real (volume ((pair f g) ⁻¹' {x})) • x.snd) :
id ┴ ┴ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘
src ┴ └─────────────┘ └────┘ └──┘ └─┘ ┴ ┴ └──┘
typ ┴ ┴ ┴ └─────────────┘ └────┘ └──┘ ┴ ┴ └─┘ ┴┴ ┴ ┴└──┘
doc └─────────────┘ └──┘ └─┘
343 by rw finset.sum_add_distrib
id └────────────────────┘
src └─┘└────────────────────┘┴
typ └─┘└────────────────────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st └─────────────────────────┘
344 ... = ((pair f g).map prod.fst).bintegral + ((pair f g).map prod.snd).bintegral :
id └──┘ ┴ ┴ └─┘ └──────┘ └───────┘ ┴ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘
src └──┘ └─┘ └──────┘ └───────┘ ┴ └──┘ └─┘ └──────┘ └───────┘
typ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘ ┴ └──┘ ┴ ┴ └─┘ └──────┘ └───────┘
doc └──┘ └─┘ └───────┘ └──┘ └─┘ └───────┘
345 begin
st └─────
346 rw [map_bintegral (pair f g), map_bintegral (pair f g)],
id └───────────┘ └──┘ ┴ ┴ └───────────┘ └──┘ ┴ ┴
src └──┘└───────────┘┴ └──┘┴ ┴ └─┘└───────────┘┴ └──┘┴ ┴ └┘
typ └──┘└───────────┘┴ └──┘┴┴┴┴└─┘└───────────┘┴ └──┘┴┴┴┴└┘
doc └──┘└───────────┘┴ └──┘┴ ┴ └─┘└───────────┘┴ └──┘┴ ┴ └┘
txt └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
par └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
pid └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘
st ─────────────────────────────┘└────────────────────────┘└──
347 { exact integrable_pair hf hg }, { refl },
id └─────────────┘ └┘ └┘
src └────┘└─────────────┘┴ ┴ ┴ └───┘
typ └────┘└─────────────┘┴└┘┴└┘┴ └───┘
doc └────┘ ┴ ┴ ┴ └───┘
txt └────┘ ┴ ┴ ┴ └───┘
par └────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────────────┘└┘└─┘└───┘└┘└
348 { exact integrable_pair hf hg }, { refl }
id └─────────────┘ └┘ └┘
src └────┘└─────────────┘┴ ┴ ┴ └───┘
typ └────┘└─────────────┘┴└┘┴└┘┴ └───┘
doc └────┘ ┴ ┴ ┴ └───┘
txt └────┘ ┴ ┴ ┴ └───┘
par └────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ ┴
st ───┘└──────────────────────────┘└┘└──────┘└─
349 end
st ──┘
350 ... = bintegral f + bintegral g : rfl
id └───────┘ ┴ ┴ └───────┘ ┴ └─┘
src └───────┘ ┴ └───────┘ └─┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └─┘
doc └───────┘ └───────┘
351
352 lemma bintegral_neg {f : α →ₛ β} (hf : integrable f) : bintegral (-f) = - bintegral f :=
id ┴ └┘ ┴ └────────┘ ┴ └───────┘ ┴┴ ┴ ┴ └───────┘ ┴
src └┘ └────────┘ └───────┘ ┴ ┴ ┴ └───────┘
typ ┴ └┘ ┴ └────────┘ ┴ └───────┘ ┴┴ ┴ ┴ └───────┘ ┴
doc └┘ └────────┘ └───────┘ └───────┘
353 calc bintegral (-f) = bintegral (f.map (has_neg.neg)) : rfl
id └───────┘ ┴┴ └───────┘ ┴└──┘ └─────────┘ └─┘
src └───────┘ ┴ └───────┘ └──┘ └─────────┘ └─┘
typ └───────┘ ┴┴ └───────┘ ┴└──┘ └─────────┘ └─┘
doc └───────┘ └───────┘ └──┘
354 ... = - bintegral f :
id ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ └───────┘ ┴
doc └───────┘
355 begin
st └─────
356 rw [map_bintegral f _ hf neg_zero, bintegral, ← sum_neg_distrib],
id └───────────┘ ┴ └┘ └──────┘ └───────┘ └─────────────┘
src └──┘└───────────┘┴ └─┘ ┴└──────┘└┘└───────┘└──┘└─────────────┘┴
typ └──┘└───────────┘┴┴└─┘└┘┴└──────┘└┘└───────┘└──┘└─────────────┘┴
doc └──┘└───────────┘┴ └─┘ ┴ └┘└───────┘└──┘ ┴
txt └──┘ ┴ └─┘ ┴ └┘ └──┘ ┴
par └──┘ ┴ └─┘ ┴ └┘ └──┘ ┴
pid └┘ ┴ └─┘ ┴ └┘ └──┘ ┴
st ────────────────────────────────────┘└─────────┘└─────────────────┘└──
357 refine finset.sum_congr rfl (λx h, smul_neg _ _),
id └──────────────┘ └─┘ └──────┘
src └─────┘└──────────────┘┴└─┘┴ └───┘└──────┘└───┘
typ └─────┘└──────────────┘┴└─┘┴ └───┘└──────┘└───┘
doc └─────┘ ┴ ┴ └───┘ └───┘
txt └─────┘ ┴ ┴ └───┘ └───┘
par └─────┘ ┴ ┴ └───┘ └───┘
pid ┴ ┴ ┴ └───┘ └───┘
st ───────────────────────────────────────────────────┘└─
358 end
st ────┘
359
360 lemma bintegral_sub {f g : α →ₛ β} (hf : integrable f) (hg : integrable g) :
id ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
src └┘ └────────┘ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴ └────────┘ ┴
doc └┘ └────────┘ └────────┘
361 bintegral (f - g) = bintegral f - bintegral g :=
id └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
doc └───────┘ └───────┘ └───────┘
362 begin
st └─────
363 have : f - g = f + (-g) := rfl,
id ┴ ┴ ┴ ┴ ┴┴ └─┘
src └─────┘ ┴┴┴ ┴┴┴ ┴┴┴ ┴ └───┘└─┘
typ └─────┘ ┴┴┴ ┴┴┴┴┴┴┴ ┴┴└───┘└─┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘
st ───────────────────────────────┘└─
364 rw [this, bintegral_add hf _, bintegral_neg hg],
id └──┘ └───────────┘ └┘ └───────────┘ └┘
src └──┘ └┘└───────────┘┴ └──┘└───────────┘┴ ┴
typ └──┘└──┘└┘└───────────┘┴└┘└──┘└───────────┘┴└┘┴
doc └──┘ └┘ ┴ └──┘ ┴ ┴
txt └──┘ └┘ ┴ └──┘ ┴ ┴
par └──┘ └┘ ┴ └──┘ ┴ ┴
pid └┘ └┘ ┴ └──┘ ┴ ┴
st ─────────┘└──────────────────┘└────────────────┘└──
365 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
366 exact hg.neg
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────┘
367 end
st └─┘
368
369 lemma bintegral_smul (r : ℝ) {f : α →ₛ β} (hf : integrable f) :
id ┴ ┴ └┘ ┴ └────────┘ ┴
src ┴ └┘ └────────┘
typ ┴ ┴ └┘ ┴ └────────┘ ┴
doc └┘ └────────┘
370 bintegral (r • f) = r • bintegral f :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └───────┘ └───────┘
371 calc bintegral (r • f) = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • r • x) :
id └───────┘ ┴ ┴ ┴ └─┘ ┴└────┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ └────┘ └─────────────┘ └────┘ └─┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └─┘ ┴└────┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴
doc └───────┘ └────┘ └─────────────┘ └─┘
372 by rw [smul_eq_map r f, map_bintegral f _ hf (smul_zero _)]
id └─────────┘ ┴ ┴ └───────────┘ ┴ └┘ └───────┘
src └──┘└─────────┘┴ ┴ └┘└───────────┘┴ └─┘ ┴ └───────┘└───┘
typ └──┘└─────────┘┴┴┴┴└┘└───────────┘┴┴└─┘└┘┴ └───────┘└───┘
doc └──┘ ┴ ┴ └┘└───────────┘┴ └─┘ ┴ └───┘
txt └──┘ ┴ ┴ └┘ ┴ └─┘ ┴ └───┘
par └──┘ ┴ ┴ └┘ ┴ └─┘ ┴ └───┘
pid └┘ ┴ ┴ └┘ ┴ └─┘ ┴ └──┘┴
st └──────────────────┘└──────────────────────────────────┘┴┴
373 ... = (f.range).sum (λ (x : β), ((ennreal.to_real (volume (f ⁻¹' {x}))) * r) • x) :
id ┴└────┘ └─┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴
src └────┘ └─┘ └─────────────┘ └────┘ └─┘ ┴ ┴ ┴
typ ┴└────┘ └─┘ ┴ └─────────────┘ └────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴ ┴
doc └────┘ └─────────────┘ └─┘
374 finset.sum_congr rfl $ λb hb, by apply smul_smul
id └──────────────┘ └─┘ ┴ └┘ └───────┘
src └──────────────┘ └─┘ └────┘└───────┘┴
typ └──────────────┘ └─┘ ┴ └┘ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st └───────────────┘
375 ... = r • bintegral f :
id ┴ ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ ┴ └───────┘ ┴
doc └───────┘
376 begin
st └─────
377 rw [bintegral, smul_sum],
id └───────┘ └──────┘
src └──┘└───────┘└┘└──────┘┴
typ └──┘└───────┘└┘└──────┘┴
doc └──┘└───────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────┘└────────┘└──
378 refine finset.sum_congr rfl (λb hb, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └──────┘
typ └─────┘└──────────────┘┴└─┘┴ └──────┘
doc └─────┘ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ───────────────────────────────────────┘└─
379 rw [smul_smul, mul_comm]
id └───────┘ └──────┘
src └──┘└───────┘└┘└──────┘└┘
typ └──┘└───────┘└┘└──────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────────────┘└────────┘┴┴
380 end
st └─┘
381
382 lemma norm_bintegral_le_bintegral_norm (f : α →ₛ β) (hf : integrable f) :
id ┴ └┘ ┴ └────────┘ ┴
src └┘ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴
doc └┘ └────────┘
383 ∥f.bintegral∥ ≤ (f.map norm).bintegral :=
id ┴┴└────────┘┴ ┴ ┴└──┘ └──┘ └───────┘
src ┴ └────────┘┴ ┴ └──┘ └──┘ └───────┘
typ ┴┴└────────┘┴ ┴ ┴└──┘ └──┘ └───────┘
doc └────────┘ └──┘ └───────┘
384 begin
st └─────
385 rw map_bintegral f norm hf norm_zero,
id └───────────┘ ┴ └──┘ └┘ └───────┘
src └─┘└───────────┘┴ ┴└──┘┴ ┴└───────┘
typ └─┘└───────────┘┴┴┴└──┘┴└┘┴└───────┘
doc └─┘└───────────┘┴ ┴ ┴ ┴
txt └─┘ ┴ ┴ ┴ ┴
par └─┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
386 rw bintegral,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘└───────┘
txt └─┘
par └─┘
pid ┴
st ─────────────┘└─
387 calc ∥sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • x)∥ ≤
id └──┘ ┴ └─┘ ┴ ┴
src └──┘ └─┘ ┴ ┴
typ └──┘ ┴ └─┘ ┴ ┴
doc └──┘ └─┘
st ──────────────────────────────────────────────────────────────────────
388 sum f.range (λx, ∥ennreal.to_real (volume (f ⁻¹' {x})) • x∥) :
id ┴
typ ┴
st ──────────────────────────────────────────────────────────────────────
389 norm_sum_le _ _
id └─────────┘
src └─────────┘
typ └─────────┘
st ────────────────────
390 ... = sum f.range (λx, ennreal.to_real (volume (f ⁻¹' {x})) • ∥x∥) :
id └─┘ └─────┘ ┴ └─────────────┘ └────┘ ┴
src └─┘ └─────┘ └─────────────┘ └────┘
typ └─┘ └─────┘ ┴ └─────────────┘ └────┘ ┴
doc └─────┘ └─────────────┘
st ─────────────────────────────────────────────────────────────────────────
391 begin
st ───┘└─────
392 refine finset.sum_congr rfl (λb hb, _),
id └──────────────┘ └─┘
src └─────┘└──────────────┘┴└─┘┴ └──────┘
typ └─────┘└──────────────┘┴└─┘┴ └──────┘
doc └─────┘ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ───────────────────────────────────────────┘└─
393 rw [norm_smul, smul_eq_mul, real.norm_eq_abs, abs_of_nonneg to_real_nonneg]
id └───────┘ └─────────┘ └──────────────┘ └───────────┘ └────────────┘
src └──┘└───────┘└┘└─────────┘└┘└──────────────┘└┘└───────────┘┴└────────────┘└─
typ └──┘└───────┘└┘└─────────┘└┘└──────────────┘└┘└───────────┘┴└────────────┘└─
doc └──┘ └┘ └┘ └┘ ┴ └─
txt └──┘ └┘ └┘ └┘ ┴ └─
par └──┘ └┘ └┘ └┘ ┴ └─
pid └┘ └┘ └┘ └┘ ┴ ┴└
st ──────────────────┘└───────────┘└────────────────┘└────────────────────────────┘┴└
394 end
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└───
395 end
st ──┘
396
397 end bintegral
398
399 end simple_func
400
401 namespace l1
402
403 open ae_eq_fun
404
405 variables [normed_group β] [second_countable_topology β]
id └──────────┘ └───────────────────────┘
src └──────────┘ └───────────────────────┘
typ └──────────┘ └───────────────────────┘
doc └──────────┘ └───────────────────────┘
406 [normed_group γ] [second_countable_topology γ]
id └──────────┘ └───────────────────────┘
src └──────────┘ └───────────────────────┘
typ └──────────┘ └───────────────────────┘
doc └──────────┘ └───────────────────────┘
407
408 variables (α β)
409 /-- `l1.simple_func` is a subspace of L1 consisting of equivalence classes of an integrable simple
410 function. -/
411 def simple_func : Type (max u v) :=
412 { f : α →₁ β // ∃ (s : α →ₛ β), integrable s ∧ ae_eq_fun.mk s s.measurable = f}
id ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ ┴ ┴
src ┴ └┘ ┴ └┘ ┴ └────────┘ ┴ └──────────┘ └─────────┘ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ ┴ ┴
doc └┘ └┘ └────────┘ └──────────┘ └─────────┘
413
414 variables {α β}
415
416 infixr ` →₁ₛ `:25 := measure_theory.l1.simple_func
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
doc └───────────────────────────┘
417
418 namespace simple_func
419
420 section instances
421 /-! Simple functions in L1 space form a `normed_space`. -/
422
423 instance : has_coe (α →₁ₛ β) (α →₁ β) := ⟨subtype.val⟩
id └─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └─────────┘
src └─────┘ └─┘ └┘ └─────────┘
typ └─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └─────────┘
doc └─┘ └┘
424
425 protected lemma eq {f g : α →₁ₛ β} : (f : α →₁ β) = (g : α →₁ β) → f = g := subtype.eq
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘
src └─┘ └┘ ┴ └┘ ┴ └────────┘
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘
doc └─┘ └┘ └┘
426 protected lemma eq' {f g : α →₁ₛ β} : (f : α →ₘ β) = (g : α →ₘ β) → f = g := subtype.eq ∘ subtype.eq
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘
src └─┘ └┘ ┴ └┘ ┴ └────────┘ ┴ └────────┘
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘
doc └─┘ └┘ └┘
427
428 @[elim_cast] protected lemma eq_iff {f g : α →₁ₛ β} : (f : α →₁ β) = (g : α →₁ β) ↔ f = g :=
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘ ┴ └┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └─┘ └┘ └┘
429 iff.intro (subtype.eq) (congr_arg coe)
id └───────┘ └────────┘ └───────┘ └─┘
src └───────┘ └────────┘ └───────┘ └─┘
typ └───────┘ └────────┘ └───────┘ └─┘
430
431 @[elim_cast] protected lemma eq_iff' {f g : α →₁ₛ β} : (f : α →ₘ β) = (g : α →ₘ β) ↔ f = g :=
id ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘ ┴ └┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └─┘ └┘ └┘
432 iff.intro (simple_func.eq') (congr_arg _)
id └───────┘ └─────────────┘ └───────┘
src └───────┘ └─────────────┘ └───────┘
typ └───────┘ └─────────────┘ └───────┘
433
434 /-- L1 simple functions forms a `emetric_space`, with the emetric being inherited from L1 space,
435 i.e., `edist f g = ∫⁻ a, edist (f a) (g a)`.
436 Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
437 integral. -/
438 protected def emetric_space : emetric_space (α →₁ₛ β) := subtype.emetric_space
id └───────────┘ ┴ └─┘ ┴ └───────────────────┘
src └───────────┘ └─┘ └───────────────────┘
typ └───────────┘ ┴ └─┘ ┴ └───────────────────┘
doc └───────────┘ └─┘ └───────────────────┘
439
440 /-- L1 simple functions forms a `metric_space`, with the metric being inherited from L1 space,
441 i.e., `dist f g = ennreal.to_real (∫⁻ a, edist (f a) (g a)`).
442 Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
443 integral. -/
444 protected def metric_space : metric_space (α →₁ₛ β) := subtype.metric_space
id └──────────┘ ┴ └─┘ ┴ └──────────────────┘
src └──────────┘ └─┘ └──────────────────┘
typ └──────────┘ ┴ └─┘ ┴ └──────────────────┘
doc └──────────┘ └─┘
445
446 local attribute [instance] protected lemma is_add_subgroup : is_add_subgroup
id └─────────────┘
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
447 (λf:α →₁ β, ∃ (s : α →ₛ β), integrable s ∧ ae_eq_fun.mk s s.measurable = f) :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ ┴ ┴
src └┘ ┴ └┘ ┴ └────────┘ ┴ └──────────┘ └─────────┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └────────┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ ┴ ┴
doc └┘ └┘ └────────┘ └──────────┘ └─────────┘
448 { zero_mem := by { use 0, split, { apply integrable_zero }, { refl } },
id └─────────────┘
src └───┘ └───┘ └────┘└─────────────┘┴ └───┘
typ └───┘ └───┘ └────┘└─────────────┘┴ └───┘
doc └───┘ └───┘ └────┘ ┴ └───┘
txt └───┘ └───┘ └────┘ ┴ └───┘
par └───┘ └───┘ └────┘ ┴ └───┘
pid ┴┴ ┴ ┴ ┴
st └──────┘└─────┘└──┘└────────────────────┘└┘└──────┘└──┘
449 add_mem :=
450 begin
st └─────
451 rintros f g ⟨s, hsi, hs⟩ ⟨t, hti, ht⟩,
src └───────────────────────────────────┘
typ └───────────────────────────────────┘
doc └───────────────────────────────────┘
txt └───────────────────────────────────┘
par └───────────────────────────────────┘
pid └────────────────────────────┘
st ────────────────────────────────────────┘└─
452 use s + t, split,
id ┴ ┴ ┴
src └──┘ ┴┴┴ └───┘
typ └──┘┴┴┴┴┴ └───┘
doc └──┘ ┴ ┴ └───┘
txt └──┘ ┴ ┴ └───┘
par └──┘ ┴ ┴ └───┘
pid ┴ ┴ ┴
st ────────────┘└─────┘└─
453 { exact hsi.add s.measurable t.measurable hti },
id └─────┘ └──────────┘ └──────────┘ └─┘
src └────┘└─────┘┴└──────────┘┴└──────────┘┴ ┴
typ └────┘└─────┘┴└──────────┘┴└──────────┘┴└─┘┴
doc └────┘ ┴└──────────┘┴└──────────┘┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────┘└──────────────────────────────────────────┘└┘└
454 { rw [coe_add, ← hs, ← ht], refl }
id └─────┘ └┘ └┘
src └──┘└─────┘└──┘ └──┘ ┴ └───┘
typ └──┘└─────┘└──┘└┘└──┘└┘┴ └───┘
doc └──┘ └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ └──┘ ┴ ┴
st ────────────────┘└────┘└────┘└──────┘└─
455 end,
st ────┘
456 neg_mem :=
457 begin
st └─────
458 rintros f ⟨s, hsi, hs⟩,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └─────────────┘
st ─────────────────────────┘└─
459 use -s, split,
id ┴┴
src └──┘┴ └───┘
typ └──┘┴┴ └───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴
st ─────────┘└─────┘└─
460 { exact hsi.neg },
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└────────────┘└┘└
461 { rw [coe_neg, ← hs], refl }
id └─────┘ └┘
src └──┘└─────┘└──┘ ┴ └───┘
typ └──┘└─────┘└──┘└┘┴ └───┘
doc └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ ┴ ┴
st ────────────────┘└────┘└──────┘└─
462 end }
st ────┘
463
464 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
465 integral. -/
466 protected def add_comm_group : add_comm_group (α →₁ₛ β) := subtype.add_comm_group
id └────────────┘ ┴ └─┘ ┴ └────────────────────┘
src └────────────┘ └─┘ └────────────────────┘
typ └────────────┘ ┴ └─┘ ┴ └────────────────────┘
doc └─┘
467
468 local attribute [instance] simple_func.add_comm_group simple_func.metric_space
id └────────────────────────┘ └──────────────────────┘
src └────────────────────────┘ └──────────────────────┘
typ └────────────────────────┘ └──────────────────────┘
doc └────────────────────────┘ └──────────────────────┘
469 simple_func.emetric_space
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
470
471 instance : inhabited (α →₁ₛ β) := ⟨0⟩
id └───────┘ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ └─┘ ┴
doc └─┘
472
473 @[simp, elim_cast] lemma coe_zero : ((0 : α →₁ₛ β) : α →₁ β) = 0 := rfl
id ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘
src └─┘ └┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘
doc └──┘ └───────┘ └─┘ └┘
474 @[simp, move_cast] lemma coe_add (f g : α →₁ₛ β) : ((f + g : α →₁ₛ β) : α →₁ β) = f + g := rfl
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └─┘ ┴ └─┘ └┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───────┘ └─┘ └─┘ └┘
475 @[simp, move_cast] lemma coe_neg (f : α →₁ₛ β) : ((-f : α →₁ₛ β) : α →₁ β) = -f := rfl
id ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─┘
src └─┘ ┴ └─┘ └┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─┘
doc └──┘ └───────┘ └─┘ └─┘ └┘
476 @[simp, move_cast] lemma coe_sub (f g : α →₁ₛ β) : ((f - g : α →₁ₛ β) : α →₁ β) = f - g := rfl
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └─┘ ┴ └─┘ └┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───────┘ └─┘ └─┘ └┘
477 @[simp] lemma edist_eq (f g : α →₁ₛ β) : edist f g = edist (f : α →₁ β) (g : α →₁ β) := rfl
id ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └─┘ └───┘ ┴ └───┘ └┘ └┘ └─┘
typ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └─┘ └┘ └┘
478 @[simp] lemma dist_eq (f g : α →₁ₛ β) : dist f g = dist (f : α →₁ β) (g : α →₁ β) := rfl
id ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └─┘ └──┘ ┴ └──┘ └┘ └┘ └─┘
typ ┴ └─┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └─┘ └┘ └┘
479
480 /-- The norm on `α →₁ₛ β` is inherited from L1 space. That is, `∥f∥ = ∫⁻ a, edist (f a) 0`.
481 Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
482 integral. -/
483 protected def has_norm : has_norm (α →₁ₛ β) := ⟨λf, ∥(f : α →₁ β)∥⟩
id └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └──────┘ └─┘ ┴ └┘ ┴
typ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └──────┘ └─┘ └┘
484
485 local attribute [instance] simple_func.has_norm
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
486
487 lemma norm_eq (f : α →₁ₛ β) : ∥f∥ = ∥(f : α →₁ β)∥ := rfl
id ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
doc └─┘ └┘
488 lemma norm_eq' (f : α →₁ₛ β) : ∥f∥ = ennreal.to_real (edist (f : α →ₘ β) 0) := rfl
id ┴ └─┘ ┴ ┴┴┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ └─┘
src └─┘ ┴ ┴ ┴ └─────────────┘ └───┘ └┘ └─┘
typ ┴ └─┘ ┴ ┴┴┴ ┴ └─────────────┘ └───┘ ┴ ┴ └┘ ┴ └─┘
doc └─┘ └─────────────┘ └┘
489
490 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
491 integral. -/
492 protected def normed_group : normed_group (α →₁ₛ β) :=
id └──────────┘ ┴ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ ┴ └─┘ ┴
doc └──────────┘ └─┘
493 normed_group.of_add_dist (λ x, rfl) $ by
id └──────────────────────┘ ┴ └─┘
src └──────────────────────┘ └─┘
typ └──────────────────────┘ ┴ └─┘
doc └──────────────────────┘
st └
494 { intros, simp only [dist_eq, coe_add, l1.dist_eq, l1.coe_add], rw edist_eq_add_add }
id └─────┘ └─────┘ └────────┘ └────────┘ └──────────────┘
src └────┘ └─────────┘└─────┘└┘└─────┘└┘└────────┘└┘└────────┘┴ └─┘└──────────────┘┴
typ └────┘ └─────────┘└─────┘└┘└─────┘└┘└────────┘└┘└────────┘┴ └─┘└──────────────┘┴
doc └────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴
txt └────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴
par └────┘ └─────────┘ └┘ └┘ └┘ ┴ └─┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴ ┴
st ─────────┘└────────────────────────────────────────────────────┘└────────────────────┘└┘
495
496 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
497
498 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
499 integral. -/
500 protected def has_scalar : has_scalar 𝕜 (α →₁ₛ β) := ⟨λk f, ⟨k • f,
id └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └─┘ ┴
typ └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └─┘
501 begin
st └─────
502 rcases f with ⟨f, ⟨s, hsi, hs⟩⟩,
id ┴
src └─────┘ └─────────────────────┘
typ └─────┘┴└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ────────────────────────────────┘└─
503 use k • s, split,
id ┴ ┴ ┴
src └──┘ ┴┴┴ └───┘
typ └──┘┴┴┴┴┴ └───┘
doc └──┘ ┴ ┴ └───┘
txt └──┘ ┴ ┴ └───┘
par └──┘ ┴ ┴ └───┘
pid ┴ ┴ ┴
st ──────────┘└─────┘└─
504 { exact integrable.smul _ hsi },
id └─────────────┘ └─┘
src └────┘└─────────────┘└─┘ ┴
typ └────┘└─────────────┘└─┘└─┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───┘└──────────────────────────┘└┘└
505 { rw [coe_smul, subtype.coe_mk, ← hs], refl }
id └──────┘ └────────────┘ └┘
src └──┘└──────┘└┘└────────────┘└──┘ ┴ └───┘
typ └──┘└──────┘└┘└────────────┘└──┘└┘┴ └───┘
doc └──┘ └┘ └──┘ ┴ └───┘
txt └──┘ └┘ └──┘ ┴ └───┘
par └──┘ └┘ └──┘ ┴ └───┘
pid └┘ └┘ └──┘ ┴ ┴
st ───────────────┘└──────────────┘└────┘└──────┘└─
506 end ⟩⟩
st ──┘
507
508 local attribute [instance, priority 10000] simple_func.has_scalar
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
509
510 @[simp, move_cast] lemma coe_smul (c : 𝕜) (f : α →₁ₛ β) :
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
doc └──┘ └───────┘ └─┘
511 ((c • f : α →₁ₛ β) : α →₁ β) = c • (f : α →₁ β) := rfl
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
src ┴ └─┘ └┘ ┴ ┴ └┘ └─┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘
doc └─┘ └┘ └┘
512
513 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
514 integral. -/
515 protected def semimodule : semimodule 𝕜 (α →₁ₛ β) :=
id └────────┘ ┴ ┴ └─┘ ┴
src └────────┘ └─┘
typ └────────┘ ┴ ┴ └─┘ ┴
doc └────────┘ └─┘
516 { one_smul := λf, simple_func.eq (by { simp only [coe_smul], exact one_smul _ _ }),
id ┴ └────────────┘ └──────┘ └──────┘
src └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└───┘
typ ┴ └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└───┘
doc └─────────┘ ┴ └────┘ └───┘
txt └─────────┘ ┴ └────┘ └───┘
par └─────────┘ ┴ └────┘ └───┘
pid ┴└──┘└┘ ┴ ┴ └──┘┴
st └─────────────────────┘└───────────────────┘└┘
517 mul_smul := λx y f, simple_func.eq (by { simp only [coe_smul], exact mul_smul _ _ _ }),
id ┴ ┴ ┴ └────────────┘ └──────┘ └──────┘
src └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ ┴ └────┘ └─────┘
txt └─────────┘ ┴ └────┘ └─────┘
par └─────────┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ ┴ ┴ └────┘┴
st └─────────────────────┘└─────────────────────┘└┘
518 smul_add := λx f g, simple_func.eq (by { simp only [coe_smul, coe_add], exact smul_add _ _ _ }),
id ┴ ┴ ┴ └────────────┘ └──────┘ └─────┘ └──────┘
src └────────────┘ └─────────┘└──────┘└┘└─────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └────────────┘ └─────────┘└──────┘└┘└─────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ └┘ ┴ └────┘ └─────┘
txt └─────────┘ └┘ ┴ └────┘ └─────┘
par └─────────┘ └┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ └┘ ┴ ┴ └────┘┴
st └──────────────────────────────┘└─────────────────────┘└┘
519 smul_zero := λx, simple_func.eq (by { simp only [coe_zero, coe_smul], exact smul_zero _ }),
id ┴ └────────────┘ └──────┘ └──────┘ └───────┘
src └────────────┘ └─────────┘└──────┘└┘└──────┘┴ └────┘└───────┘└─┘
typ ┴ └────────────┘ └─────────┘└──────┘└┘└──────┘┴ └────┘└───────┘└─┘
doc └─────────┘ └┘ ┴ └────┘ └─┘
txt └─────────┘ └┘ ┴ └────┘ └─┘
par └─────────┘ └┘ ┴ └────┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴ └┘┴
st └───────────────────────────────┘└──────────────────┘└┘
520 add_smul := λx y f, simple_func.eq (by { simp only [coe_smul], exact add_smul _ _ _ }),
id ┴ ┴ ┴ └────────────┘ └──────┘ └──────┘
src └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
typ ┴ ┴ ┴ └────────────┘ └─────────┘└──────┘┴ └────┘└──────┘└─────┘
doc └─────────┘ ┴ └────┘ └─────┘
txt └─────────┘ ┴ └────┘ └─────┘
par └─────────┘ ┴ └────┘ └─────┘
pid ┴└──┘└┘ ┴ ┴ └────┘┴
st └─────────────────────┘└─────────────────────┘└┘
521 zero_smul := λf, simple_func.eq (by { simp only [coe_smul], exact zero_smul _ _ }) }
id ┴ └────────────┘ └──────┘ └───────┘
src └────────────┘ └─────────┘└──────┘┴ └────┘└───────┘└───┘
typ ┴ └────────────┘ └─────────┘└──────┘┴ └────┘└───────┘└───┘
doc └─────────┘ ┴ └────┘ └───┘
txt └─────────┘ ┴ └────┘ └───┘
par └─────────┘ ┴ └────┘ └───┘
pid ┴└──┘└┘ ┴ ┴ └──┘┴
st └─────────────────────┘└────────────────────┘└┘
522
523 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
524 integral. -/
525 protected def module : module 𝕜 (α →₁ₛ β) :=
id └────┘ ┴ ┴ └─┘ ┴
src └────┘ └─┘
typ └────┘ ┴ ┴ └─┘ ┴
doc └────┘ └─┘
526 { .. simple_func.semimodule }
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
527
528 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
529 integral. -/
530 protected def vector_space : vector_space 𝕜 (α →₁ₛ β) :=
id └──────────┘ ┴ ┴ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ ┴ ┴ └─┘ ┴
doc └──────────┘ └─┘
531 { .. simple_func.semimodule }
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
532
533 local attribute [instance] simple_func.vector_space simple_func.normed_group
id └──────────────────────┘ └──────────────────────┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ └──────────────────────┘
doc └──────────────────────┘ └──────────────────────┘
534
535 /-- Not declared as an instance as `α →₁ₛ β` will only be useful in the construction of the bochner
536 integral. -/
537 protected def normed_space : normed_space 𝕜 (α →₁ₛ β) :=
id └──────────┘ ┴ ┴ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ ┴ ┴ └─┘ ┴
doc └──────────┘ └─┘
538 ⟨ λc f, by { rw [norm_eq, norm_eq, coe_smul, norm_smul] } ⟩
id ┴ ┴ └─────┘ └─────┘ └──────┘ └───────┘
src └──┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘
typ ┴ ┴ └──┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st └────────────┘└───────┘└────────┘└─────────┘┴┴└┘
539
540 end instances
541
542 local attribute [instance] simple_func.normed_group simple_func.normed_space
id └──────────────────────┘ └──────────────────────┘
src └──────────────────────┘ └──────────────────────┘
typ └──────────────────────┘ └──────────────────────┘
doc └──────────────────────┘ └──────────────────────┘
543
544 section of_simple_func
545
546 /-- Construct the equivalence class `[f]` of an integrable simple function `f`. -/
547 @[reducible] def of_simple_func (f : α →ₛ β) (hf : integrable f) : (α →₁ₛ β) :=
id ┴ └┘ ┴ └────────┘ ┴ ┴ └─┘ ┴
src └┘ └────────┘ └─┘
typ ┴ └┘ ┴ └────────┘ ┴ ┴ └─┘ ┴
doc └───────┘ └┘ └────────┘ └─┘
548 ⟨l1.of_fun f f.measurable hf, ⟨f, ⟨hf, rfl⟩⟩⟩
id └───────┘ ┴ ┴└─────────┘ └┘ ┴ └┘ └─┘
src └───────┘ └─────────┘ └─┘
typ └───────┘ ┴ ┴└─────────┘ └┘ ┴ └┘ └─┘
doc └───────┘ └─────────┘
549
550 lemma of_simple_func_eq_of_fun (f : α →ₛ β) (hf : integrable f) :
id ┴ └┘ ┴ └────────┘ ┴
src └┘ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴
doc └┘ └────────┘
551 (of_simple_func f hf : α →₁ β) = l1.of_fun f f.measurable hf := rfl
id └────────────┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴└─────────┘ └┘ └─┘
src └────────────┘ └┘ ┴ └───────┘ └─────────┘ └─┘
typ └────────────┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴└─────────┘ └┘ └─┘
doc └────────────┘ └┘ └───────┘ └─────────┘
552
553 lemma of_simple_func_eq_mk (f : α →ₛ β) (hf : integrable f) :
id ┴ └┘ ┴ └────────┘ ┴
src └┘ └────────┘
typ ┴ └┘ ┴ └────────┘ ┴
doc └┘ └────────┘
554 (of_simple_func f hf : α →ₘ β) = ae_eq_fun.mk f f.measurable := rfl
id └────────────┘ ┴ └┘ ┴ └┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ └─┘
src └────────────┘ └┘ ┴ └──────────┘ └─────────┘ └─┘
typ └────────────┘ ┴ └┘ ┴ └┘ ┴ ┴ └──────────┘ ┴ ┴└─────────┘ └─┘
doc └────────────┘ └┘ └──────────┘ └─────────┘
555
556 lemma of_simple_func_zero : of_simple_func (0 : α →ₛ β) (integrable_zero α β) = 0 := rfl
id └────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
src └────────────┘ └┘ └─────────────┘ ┴ └─┘
typ └────────────┘ ┴ └┘ ┴ └─────────────┘ ┴ ┴ ┴ └─┘
doc └────────────┘ └┘
557
558 lemma of_simple_func_add (f g : α →ₛ β) (hf hg) :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
559 of_simple_func (f + g) (integrable.add f.measurable hf g.measurable hg) = of_simple_func f hf +
id └────────────┘ ┴ ┴ ┴ └────────────┘ ┴└─────────┘ └┘ ┴└─────────┘ └┘ ┴ └────────────┘ ┴ └┘ ┴
src └────────────┘ ┴ └────────────┘ └─────────┘ └─────────┘ ┴ └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴└─────────┘ └┘ ┴└─────────┘ └┘ ┴ └────────────┘ ┴ └┘ ┴
doc └────────────┘ └─────────┘ └─────────┘ └────────────┘
560 of_simple_func g hg := rfl
id └────────────┘ ┴ └┘ └─┘
src └────────────┘ └─┘
typ └────────────┘ ┴ └┘ └─┘
doc └────────────┘
561
562 lemma of_simple_func_neg (f : α →ₛ β) (hf) :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
563 of_simple_func (-f) (integrable.neg hf) = -of_simple_func f hf := rfl
id └────────────┘ ┴┴ └────────────┘ └┘ ┴ ┴└────────────┘ ┴ └┘ └─┘
src └────────────┘ ┴ └────────────┘ ┴ ┴└────────────┘ └─┘
typ └────────────┘ ┴┴ └────────────┘ └┘ ┴ ┴└────────────┘ ┴ └┘ └─┘
doc └────────────┘ └────────────┘
564
565 lemma of_simple_func_sub (f g : α →ₛ β) (hf hg) :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
566 of_simple_func (f - g) (integrable.sub f.measurable hf g.measurable hg) = of_simple_func f hf -
id └────────────┘ ┴ ┴ ┴ └────────────┘ ┴└─────────┘ └┘ ┴└─────────┘ └┘ ┴ └────────────┘ ┴ └┘ ┴
src └────────────┘ ┴ └────────────┘ └─────────┘ └─────────┘ ┴ └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴└─────────┘ └┘ ┴└─────────┘ └┘ ┴ └────────────┘ ┴ └┘ ┴
doc └────────────┘ └─────────┘ └─────────┘ └────────────┘
567 of_simple_func g hg := rfl
id └────────────┘ ┴ └┘ └─┘
src └────────────┘ └─┘
typ └────────────┘ ┴ └┘ └─┘
doc └────────────┘
568
569 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
570
571 lemma of_simple_func_smul (f : α →ₛ β) (hf) (c : 𝕜) :
id ┴ └┘ ┴ ┴
src └┘
typ ┴ └┘ ┴ ┴
doc └┘
572 of_simple_func (c • f) (integrable.smul _ hf) = c • of_simple_func f hf := rfl
id └────────────┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └─┘
src └────────────┘ ┴ └─────────────┘ ┴ ┴ └────────────┘ └─┘
typ └────────────┘ ┴ ┴ ┴ └─────────────┘ └┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ └─┘
doc └────────────┘ └────────────┘
573
574 lemma norm_of_simple_func (f : α →ₛ β) (hf) : ∥of_simple_func f hf∥ = ennreal.to_real (∫⁻ a, edist (f a) 0) :=
id ┴ └┘ ┴ ┴└────────────┘ ┴ └┘┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴ ┴
src └┘ ┴└────────────┘ ┴ ┴ └─────────────┘ └┘ ┴ └───┘
typ ┴ └┘ ┴ ┴└────────────┘ ┴ └┘┴ ┴ └─────────────┘ └┘ ┴┴ └───┘ ┴ ┴
doc └┘ └────────────┘ └─────────────┘ └┘ ┴
575 rfl
id └─┘
src └─┘
typ └─┘
576
577 end of_simple_func
578
579 section to_simple_func
580
581 /-- Find a representative of a `l1.simple_func`. -/
582 def to_simple_func (f : α →₁ₛ β) : α →ₛ β := classical.some f.2
id ┴ └─┘ ┴ ┴ └┘ ┴ └────────────┘ ┴┴
src └─┘ └┘ └────────────┘ ┴
typ ┴ └─┘ ┴ ┴ └┘ ┴ └────────────┘ ┴┴
doc └─┘ └┘
583
584 /-- `f.to_simple_func` is measurable. -/
585 protected lemma measurable (f : α →₁ₛ β) : measurable f.to_simple_func := f.to_simple_func.measurable
id ┴ └─┘ ┴ └────────┘ ┴└─────────────┘ ┴└─────────────┘└─────────┘
src └─┘ └────────┘ └─────────────┘ └─────────────┘└─────────┘
typ ┴ └─┘ ┴ └────────┘ ┴└─────────────┘ ┴└─────────────┘└─────────┘
doc └─┘ └────────┘ └─────────────┘ └─────────────┘└─────────┘
586
587 /-- `f.to_simple_func` is integrable. -/
588 protected lemma integrable (f : α →₁ₛ β) : integrable f.to_simple_func :=
id ┴ └─┘ ┴ └────────┘ ┴└─────────────┘
src └─┘ └────────┘ └─────────────┘
typ ┴ └─┘ ┴ └────────┘ ┴└─────────────┘
doc └─┘ └────────┘ └─────────────┘
589 let ⟨h, _⟩ := classical.some_spec f.2 in h
id └─┘ ┴ └─────────────────┘ ┴┴
src └─────────────────┘ ┴
typ └─┘ ┴ └─────────────────┘ ┴┴
590
591 lemma of_simple_func_to_simple_func (f : α →₁ₛ β) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └─┘
592 of_simple_func (f.to_simple_func) f.integrable = f :=
id └────────────┘ ┴└─────────────┘ ┴└─────────┘ ┴ ┴
src └────────────┘ └─────────────┘ └─────────┘ ┴
typ └────────────┘ ┴└─────────────┘ ┴└─────────┘ ┴ ┴
doc └────────────┘ └─────────────┘ └─────────┘
593 by { rw ← simple_func.eq_iff', exact (classical.some_spec f.2).2 }
id └─────────────────┘ └─────────────────┘ ┴
src └───┘└─────────────────┘ └────┘ └─────────────────┘┴ └────┘
typ └───┘└─────────────────┘ └────┘ └─────────────────┘┴┴└────┘
doc └───┘ └────┘ ┴ └────┘
txt └───┘ └────┘ ┴ └────┘
par └───┘ └────┘ ┴ └────┘
pid └─┘ ┴ ┴ └─┘└─┘
st └─────────────────────────┘└──────────────────────────────────┘└┘
594
595 lemma to_simple_func_of_simple_func (f : α →ₛ β) (hfi) :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
596 ∀ₘ a, (of_simple_func f hfi).to_simple_func a = f a :=
id └┘ ┴┴ └────────────┘ ┴ └─┘ └────────────┘ ┴ ┴ ┴ ┴
src └┘ ┴ └────────────┘ └────────────┘ ┴
typ └┘ ┴┴ └────────────┘ ┴ └─┘ └────────────┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └────────────┘ └────────────┘
597 by { rw ← mk_eq_mk, exact (classical.some_spec (of_simple_func f hfi).2).2 }
id └──────┘ └─────────────────┘ └────────────┘ ┴ └─┘
src └───┘└──────┘ └────┘ └─────────────────┘┴ └────────────┘┴ ┴ └─────┘
typ └───┘└──────┘ └────┘ └─────────────────┘┴ └────────────┘┴┴┴└─┘└─────┘
doc └───┘ └────┘ ┴ └────────────┘┴ ┴ └─────┘
txt └───┘ └────┘ ┴ ┴ ┴ └─────┘
par └───┘ └────┘ ┴ ┴ ┴ └─────┘
pid └─┘ ┴ ┴ ┴ ┴ └──┘└─┘
st └──────────────┘└───────────────────────────────────────────────────────┘└┘
598
599 lemma to_simple_func_eq_to_fun (f : α →₁ₛ β) : ∀ₘ a, (f.to_simple_func) a = (f : α →₁ β).to_fun a :=
id ┴ └─┘ ┴ └┘ ┴┴ ┴└─────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴
src └─┘ └┘ ┴ └─────────────┘ ┴ └┘ └────┘
typ ┴ └─┘ ┴ └┘ ┴┴ ┴└─────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴
doc └─┘ └┘ ┴ └─────────────┘ └┘ └────┘
600 begin
st └─────
601 rw [← of_fun_eq_of_fun (f.to_simple_func) (f : α →₁ β).to_fun f.measurable f.integrable
id └──────────────┘ └──────────────┘ └┘ └──────────┘ └──────────┘
src └────┘└──────────────┘┴ └──────────────┘└┘ └─┘ ┴└┘┴ └───────┘└──────────┘┴└──────────┘└
typ └────┘└──────────────┘┴ └──────────────┘└┘ └─┘ ┴└┘┴ └───────┘└──────────┘┴└──────────┘└
doc └────┘ ┴ └──────────────┘└┘ └─┘ ┴└┘┴ └───────┘└──────────┘┴└──────────┘└
txt └────┘ ┴ └┘ └─┘ ┴ ┴ └───────┘ ┴ └
par └────┘ ┴ └┘ └─┘ ┴ ┴ └───────┘ ┴ └
pid └──┘ ┴ └┘ └─┘ ┴ ┴ └───────┘ ┴ └
st ──────────────────────────────────────────────────────────────────────────────────────────
602 (f:α→₁β).measurable (f:α→₁β).integrable, ← l1.eq_iff],
id ┴ ┴ ┴ └───────┘
src ───┘ ┴ └───────────┘ ┴ └──────────────┘└───────┘┴
typ ───┘ ┴ └───────────┘ ┴┴┴ ┴└──────────────┘└───────┘┴
doc ───┘ ┴ └───────────┘ ┴ └──────────────┘ ┴
txt ───┘ ┴ └───────────┘ ┴ └──────────────┘ ┴
par ───┘ ┴ └───────────┘ ┴ └──────────────┘ ┴
pid ───┘ ┴ └───────────┘ ┴ └──────────────┘ ┴
st ─────────────────────────────────────────┘└────────────┘└──
603 simp only [of_fun_eq_mk],
id └──────────┘
src └─────────┘└──────────┘┴
typ └─────────┘└──────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ─────────────────────────┘└─
604 rcases classical.some_spec f.2 with ⟨_, h⟩, convert h, rw mk_to_fun, refl
id └─────────────────┘ ┴ ┴ └───────┘
src └─────┘└─────────────────┘┴ └────────────┘ └──────┘ └─┘└───────┘ └───┘
typ └─────┘└─────────────────┘┴┴└────────────┘ └──────┘┴ └─┘└───────┘ └───┘
doc └─────┘ ┴ └────────────┘ └──────┘ └─┘ └───┘
txt └─────┘ ┴ └────────────┘ └──────┘ └─┘ └───┘
par └─────┘ ┴ └────────────┘ └──────┘ └─┘ └───┘
pid ┴ ┴ └────────────┘ ┴ ┴ ┴
st ───────────────────────────────────────────┘└─────────┘└────────────┘└─────┘
605 end
st └─┘
606
607 variables (α β)
608 lemma zero_to_simple_func : ∀ₘ a, (0 : α →₁ₛ β).to_simple_func a = 0 :=
id └┘ ┴┴ ┴ └─┘ ┴ └────────────┘ ┴ ┴
src └┘ ┴ └─┘ └────────────┘ ┴
typ └┘ ┴┴ ┴ └─┘ ┴ └────────────┘ ┴ ┴
doc └┘ ┴ └─┘ └────────────┘
609 begin
st └─────
610 filter_upwards [to_simple_func_eq_to_fun (0 : α →₁ₛ β), l1.zero_to_fun α β],
id └──────────────────────┘ ┴ └─┘ ┴ └────────────┘ ┴ ┴
src └──────────────┘└──────────────────────┘┴ └──┘ ┴└─┘┴ └─┘└────────────┘┴ ┴ ┴
typ └──────────────┘└──────────────────────┘┴ └──┘┴┴└─┘┴┴└─┘└────────────┘┴┴┴┴┴
doc └──────────────┘ ┴ └──┘ ┴└─┘┴ └─┘ ┴ ┴ ┴
txt └──────────────┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴
par └──────────────┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴
pid └┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
611 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
612 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
613 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
614 rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└─
615 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
616 exact h
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────┘
617 end
st └─┘
618 variables {α β}
619
620 lemma add_to_simple_func (f g : α →₁ₛ β) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └─┘
621 ∀ₘ a, (f + g).to_simple_func a = f.to_simple_func a + g.to_simple_func a :=
id └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ ┴└─────────────┘ ┴
src └┘ ┴ ┴ └────────────┘ ┴ └─────────────┘ ┴ └─────────────┘
typ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ ┴└─────────────┘ ┴
doc └┘ ┴ └────────────┘ └─────────────┘ └─────────────┘
622 begin
st └─────
623 filter_upwards [to_simple_func_eq_to_fun (f + g), to_simple_func_eq_to_fun f,
id └──────────────────────┘ ┴ ┴ ┴ └──────────────────────┘ ┴
src └──────────────┘└──────────────────────┘┴ ┴┴┴ └─┘└──────────────────────┘┴ └─
typ └──────────────┘└──────────────────────┘┴ ┴┴┴┴┴└─┘└──────────────────────┘┴┴└─
doc └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
txt └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
par └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
pid └┘ ┴ ┴ ┴ └─┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────────────
624 to_simple_func_eq_to_fun g, l1.add_to_fun (f:α→₁β) g],
id └──────────────────────┘ ┴ └───────────┘ ┴ ┴└┘┴ ┴
src ───┘└──────────────────────┘┴ └┘└───────────┘┴ ┴ └┘ └┘ ┴
typ ───┘└──────────────────────┘┴┴└┘└───────────┘┴ ┴┴┴└┘┴└┘┴┴
doc ───┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴
txt ───┘ ┴ └┘ ┴ ┴ └┘ ┴
par ───┘ ┴ └┘ ┴ ┴ └┘ ┴
pid ───┘ ┴ └┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────┘└─
625 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
626 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
627 repeat { assume h, rw h },
id ┴
src └───────┘└──────┘└┘└─┘ ┴┴
typ └───────┘└──────┘└┘└─┘┴┴┴
doc └───────┘└──────┘└┘└─┘ ┴┴
txt └───────┘└──────┘└┘└─┘ ┴┴
par └───────┘└──────┘└┘└─┘ ┴┴
pid └──────────────┘ └┘
st ──────────────────┘└─────┘└┘└
628 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
629 rw ← h,
id ┴
src └───┘
typ └───┘┴
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────┘└─
630 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
631 end
st └─┘
632
633 lemma neg_to_simple_func (f : α →₁ₛ β) : ∀ₘ a, (-f).to_simple_func a = - f.to_simple_func a :=
id ┴ └─┘ ┴ └┘ ┴┴ ┴┴ └────────────┘ ┴ ┴ ┴ ┴└─────────────┘ ┴
src └─┘ └┘ ┴ ┴ └────────────┘ ┴ ┴ └─────────────┘
typ ┴ └─┘ ┴ └┘ ┴┴ ┴┴ └────────────┘ ┴ ┴ ┴ ┴└─────────────┘ ┴
doc └─┘ └┘ ┴ └────────────┘ └─────────────┘
634 begin
st └─────
635 filter_upwards [to_simple_func_eq_to_fun (-f), to_simple_func_eq_to_fun f, l1.neg_to_fun (f:α→₁β)],
id └──────────────────────┘ ┴┴ └──────────────────────┘ ┴ └───────────┘ ┴ ┴└┘┴
src └──────────────┘└──────────────────────┘┴ ┴ └─┘└──────────────────────┘┴ └┘└───────────┘┴ ┴ └┘ └┘
typ └──────────────┘└──────────────────────┘┴ ┴┴└─┘└──────────────────────┘┴┴└┘└───────────┘┴ ┴┴┴└┘┴└┘
doc └──────────────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘ └┘
txt └──────────────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘
par └──────────────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘
pid └┘ ┴ └─┘ ┴ └┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────┘└─
636 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
637 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
638 repeat { assume h, rw h },
id ┴
src └───────┘└──────┘└┘└─┘ ┴┴
typ └───────┘└──────┘└┘└─┘┴┴┴
doc └───────┘└──────┘└┘└─┘ ┴┴
txt └───────┘└──────┘└┘└─┘ ┴┴
par └───────┘└──────┘└┘└─┘ ┴┴
pid └──────────────┘ └┘
st ──────────────────┘└─────┘└┘└
639 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
640 rw ← h,
id ┴
src └───┘
typ └───┘┴
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────┘└─
641 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
642 end
st └─┘
643
644 lemma sub_to_simple_func (f g : α →₁ₛ β) :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
doc └─┘
645 ∀ₘ a, (f - g).to_simple_func a = f.to_simple_func a - g.to_simple_func a :=
id └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ ┴└─────────────┘ ┴
src └┘ ┴ ┴ └────────────┘ ┴ └─────────────┘ ┴ └─────────────┘
typ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ ┴└─────────────┘ ┴
doc └┘ ┴ └────────────┘ └─────────────┘ └─────────────┘
646 begin
st └─────
647 filter_upwards [to_simple_func_eq_to_fun (f - g), to_simple_func_eq_to_fun f,
id └──────────────────────┘ ┴ ┴ ┴ └──────────────────────┘ ┴
src └──────────────┘└──────────────────────┘┴ ┴┴┴ └─┘└──────────────────────┘┴ └─
typ └──────────────┘└──────────────────────┘┴ ┴┴┴┴┴└─┘└──────────────────────┘┴┴└─
doc └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
txt └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
par └──────────────┘ ┴ ┴ ┴ └─┘ ┴ └─
pid └┘ ┴ ┴ ┴ └─┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────────────
648 to_simple_func_eq_to_fun g, l1.sub_to_fun (f:α→₁β) g],
id └──────────────────────┘ ┴ └───────────┘ ┴ ┴└┘┴ ┴
src ───┘└──────────────────────┘┴ └┘└───────────┘┴ ┴ └┘ └┘ ┴
typ ───┘└──────────────────────┘┴┴└┘└───────────┘┴ ┴┴┴└┘┴└┘┴┴
doc ───┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴
txt ───┘ ┴ └┘ ┴ ┴ └┘ ┴
par ───┘ ┴ └┘ ┴ ┴ └┘ ┴
pid ───┘ ┴ └┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────┘
649 assume a,
650 simp only [mem_set_of_eq],
651 repeat { assume h, rw h },
652 assume h,
653 rw ← h,
654 refl
655 end
st └─┘
656
657 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
658
659 lemma smul_to_simple_func (k : 𝕜) (f : α →₁ₛ β) :
id ┴ ┴ └─┘ ┴
src └─┘
typ ┴ ┴ └─┘ ┴
doc └─┘
660 ∀ₘ a, (k • f).to_simple_func a = k • f.to_simple_func a :=
id └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└─────────────┘ ┴
src └┘ ┴ ┴ └────────────┘ ┴ ┴ └─────────────┘
typ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴└─────────────┘ ┴
doc └┘ ┴ └────────────┘ └─────────────┘
661 begin
662 filter_upwards [to_simple_func_eq_to_fun (k • f), to_simple_func_eq_to_fun f,
663 l1.smul_to_fun k (f:α→₁β)],
664 assume a,
665 simp only [mem_set_of_eq],
666 repeat { assume h, rw h },
667 assume h,
668 rw ← h,
669 refl
670 end
st └─┘
671
672 lemma lintegral_edist_to_simple_func_lt_top (f g : α →₁ₛ β) :
id ┴ ┴
typ ┴ ┴
673 (∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func g) x)) < ⊤ :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
674 begin
675 rw lintegral_rw₂ (to_simple_func_eq_to_fun f) (to_simple_func_eq_to_fun g),
676 exact lintegral_edist_to_fun_lt_top _ _
677 end
st └─┘
678
679 lemma dist_to_simple_func (f g : α →₁ₛ β) : dist f g =
id ┴ ┴
typ ┴ ┴
680 ennreal.to_real (∫⁻ x, edist (f.to_simple_func x) (g.to_simple_func x)) :=
id └┘ └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘ └┘
681 begin
682 rw [dist_eq, l1.dist_to_fun, ennreal.to_real_eq_to_real],
683 { rw lintegral_rw₂, repeat { exact all_ae_eq_symm (to_simple_func_eq_to_fun _) } },
st └──┘
684 { exact l1.lintegral_edist_to_fun_lt_top _ _ },
st └┘
685 { exact lintegral_edist_to_simple_func_lt_top _ _ }
st └─
686 end
st ──┘
687
688 lemma norm_to_simple_func (f : α →₁ₛ β) :
id ┴ ┴
typ ┴ ┴
689 ∥f∥ = ennreal.to_real (∫⁻ (a : α), nnnorm ((to_simple_func f) a)) :=
id └┘ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘ └┘
690 calc ∥f∥ = ennreal.to_real (∫⁻x, edist (f.to_simple_func x) ((0 : α →₁ₛ β).to_simple_func x)) :
id └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘ └┘
691 begin
692 rw [← dist_zero_right, dist_to_simple_func]
st ┴
693 end
st └─┘
694 ... = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x)) :
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
doc └─────────────┘
695 begin
696 rw lintegral_nnnorm_eq_lintegral_edist,
697 have : (∫⁻ (x : α), edist ((to_simple_func f) x) ((to_simple_func (0:α→₁ₛβ)) x)) =
id ┴
typ ┴
698 ∫⁻ (x : α), edist ((to_simple_func f) x) 0,
id ┴
typ ┴
699 { apply lintegral_congr_ae, filter_upwards [zero_to_simple_func α β],
id ┴ ┴
typ ┴ ┴
700 assume a,
701 simp only [mem_set_of_eq],
702 assume h,
703 rw h },
st └┘
704 rw [ennreal.to_real_eq_to_real],
705 { exact this },
st └┘
706 { exact lintegral_edist_to_simple_func_lt_top _ _ },
st └┘
707 { rw ← this, exact lintegral_edist_to_simple_func_lt_top _ _ }
st └─
708 end
st ──┘
709
710 lemma norm_eq_bintegral (f : α →₁ₛ β) : ∥f∥ = (f.to_simple_func.map norm).bintegral :=
id ┴ ┴
typ ┴ ┴
711 calc ∥f∥ = ennreal.to_real (∫⁻ (x : α), (coe ∘ nnnorm) (f.to_simple_func x)) :
id └┘ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘ └┘
712 by { rw norm_to_simple_func }
st └┘
713 ... = (f.to_simple_func.map norm).bintegral :
714 begin
715 rw ← f.to_simple_func.bintegral_eq_lintegral (coe ∘ nnnorm) f.integrable,
716 { congr },
st └┘
717 { simp only [nnnorm_zero, function.comp_app, ennreal.coe_zero] },
st └┘
718 { assume b, exact coe_lt_top }
st └─
719 end
st ──┘
720
721 end to_simple_func
722
723 section coe_to_l1
724 /-! The embedding of integrable simple functions `α →₁ₛ β` into L1 is a uniform and dense embedding. -/
725
726 lemma exists_simple_func_near (f : α →₁ β) {ε : ℝ} (ε0 : 0 < ε) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
727 ∃ s : α →₁ₛ β, dist f s < ε :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
728 begin
729 rcases f with ⟨⟨f, hfm⟩, hfi⟩,
730 simp only [integrable_mk, quot_mk_eq_mk] at hfi,
731 rcases simple_func_sequence_tendsto' hfm hfi with ⟨F, ⟨h₁, h₂⟩⟩,
732 rw ennreal.tendsto_at_top at h₂,
733 rcases h₂ (ennreal.of_real (ε/2)) (of_real_pos.2 $ half_pos ε0) with ⟨N, hN⟩,
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └─────────────┘
734 have : (∫⁻ (x : α), nndist (F N x) (f x)) < ennreal.of_real ε :=
id ┴ ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
735 calc (∫⁻ (x : α), nndist (F N x) (f x)) ≤ 0 + ennreal.of_real (ε/2) : (hN N (le_refl _)).2
id ┴ ┴ ┴
typ ┴ ┴ ┴
736 ... < ennreal.of_real ε :
id └─────────────┘ ┴
src └─────────────┘
typ └─────────────┘ ┴
doc └─────────────┘
737 by { simp only [zero_add, of_real_lt_of_real_iff ε0], exact half_lt_self ε0 },
st └┘
738 { refine ⟨of_simple_func (F N) (h₁ N), _⟩, rw dist_comm,
id ┴
typ ┴
739 rw lt_of_real_iff_to_real_lt _ at this,
740 { simpa [edist_mk_mk', of_simple_func, l1.of_fun, l1.dist_eq] },
st └┘
741 rw ← lt_top_iff_ne_top, exact lt_trans this (by simp [lt_top_iff_ne_top, of_real_ne_top]) },
st └┘
742 { exact zero_ne_top }
st └─
743 end
st ──┘
744
745 protected lemma uniform_continuous : uniform_continuous (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
746 uniform_continuous_comap
747
748 protected lemma uniform_embedding : uniform_embedding (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
749 uniform_embedding_comap subtype.val_injective
750
751 protected lemma uniform_inducing : uniform_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
752 simple_func.uniform_embedding.to_uniform_inducing
753
754 protected lemma dense_embedding : dense_embedding (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
755 simple_func.uniform_embedding.dense_embedding $
756 λ f, mem_closure_iff_nhds.2 $ λ t ht,
757 let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
758 let ⟨s, h⟩ := exists_simple_func_near f ε0 in
759 ⟨_, hε (metric.mem_ball'.2 h), s, rfl⟩
760
761 protected lemma dense_inducing : dense_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
762 simple_func.dense_embedding.to_dense_inducing
763
764 protected lemma dense_range : dense_range (coe : (α →₁ₛ β) → (α →₁ β)) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
765 simple_func.dense_inducing.dense
766
767 variables (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 β]
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴ ┴ ┴ ┴ ┴
768
769 variables (α β)
770
771 /-- The uniform and dense embedding of L1 simple functions into L1 functions. -/
772 def coe_to_l1 : (α →₁ₛ β) →L[𝕜] (α →₁ β) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
773 { to_fun := (coe : (α →₁ₛ β) → (α →₁ β)),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
774 add := λf g, rfl,
775 smul := λk f, rfl,
id ┴
typ ┴
776 cont := l1.simple_func.uniform_continuous.continuous, }
777
778 variables {α β 𝕜}
779
780 end coe_to_l1
781
782 section pos_part
783
784 /-- Positive part of a simple function in L1 space. -/
785 def pos_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := ⟨l1.pos_part (f : α →₁ ℝ),
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
786 begin
787 rcases f with ⟨f, s, hsi, hsf⟩,
788 use s.pos_part,
789 split,
790 { exact integrable.max_zero hsi },
st └┘
791 { simp only [subtype.coe_mk],
792 rw [l1.coe_pos_part, ← hsf, ae_eq_fun.pos_part, ae_eq_fun.zero_def, comp₂_mk_mk, mk_eq_mk],
793 filter_upwards [],
794 simp only [mem_set_of_eq],
795 assume a,
796 refl }
st └─
797 end ⟩
st ──┘
798
799 /-- Negative part of a simple function in L1 space. -/
800 def neg_part (f : α →₁ₛ ℝ) : α →₁ₛ ℝ := pos_part (-f)
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
801
802 @[move_cast] lemma coe_pos_part (f : α →₁ₛ ℝ) : (f.pos_part : α →₁ ℝ) = (f : α →₁ ℝ).pos_part := rfl
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
803
804 @[move_cast] lemma coe_neg_part (f : α →₁ₛ ℝ) : (f.neg_part : α →₁ ℝ) = (f : α →₁ ℝ).neg_part := rfl
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
805
806 end pos_part
807
808 section simple_func_integral
809 /-! Define the Bochner integral on `α →₁ₛ β` and prove basic properties of this integral. -/
810
811 variables [normed_space ℝ β]
id ┴
src ┴
typ ┴
812
813 /-- The Bochner integral over simple functions in l1 space. -/
814 def integral (f : α →₁ₛ β) : β := (f.to_simple_func).bintegral
id ┴ ┴ ┴
typ ┴ ┴ ┴
815
816 lemma integral_eq_bintegral (f : α →₁ₛ β) : integral f = (f.to_simple_func).bintegral := rfl
id ┴ ┴
typ ┴ ┴
817
818 lemma integral_eq_lintegral {f : α →₁ₛ ℝ} (h_pos : ∀ₘ a, 0 ≤ f.to_simple_func a) :
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
819 integral f = ennreal.to_real (∫⁻ a, ennreal.of_real (f.to_simple_func a)) :=
id └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
doc └┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
820 by { rw [integral, simple_func.bintegral_eq_lintegral' f.integrable h_pos], refl }
st └┘
821
822 lemma integral_congr (f g : α →₁ₛ β) (h : ∀ₘ a, f.to_simple_func a = g.to_simple_func a) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
823 integral f = integral g :=
824 by { simp only [integral], apply simple_func.bintegral_congr f.integrable g.integrable, exact h }
st └┘
825
826 lemma integral_add (f g : α →₁ₛ β) : integral (f + g) = integral f + integral g :=
id ┴ ┴
typ ┴ ┴
827 begin
828 simp only [integral],
829 rw ← simple_func.bintegral_add f.integrable g.integrable,
830 apply simple_func.bintegral_congr (f + g).integrable,
831 { exact f.integrable.add f.measurable g.measurable g.integrable },
st └┘
832 { apply add_to_simple_func },
st └┘
833 end
st └─┘
834
835 lemma integral_smul (r : ℝ) (f : α →₁ₛ β) : integral (r • f) = r • integral f :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
836 begin
837 simp only [integral],
838 rw ← simple_func.bintegral_smul _ f.integrable,
839 apply simple_func.bintegral_congr (r • f).integrable,
id ┴
typ ┴
840 { exact integrable.smul _ f.integrable },
st └┘
841 { apply smul_to_simple_func }
st └─
842 end
st ──┘
843
844 lemma norm_integral_le_norm (f : α →₁ₛ β) : ∥ integral f ∥ ≤ ∥f∥ :=
id ┴ ┴
typ ┴ ┴
845 begin
846 rw [integral, norm_eq_bintegral],
847 exact f.to_simple_func.norm_bintegral_le_bintegral_norm f.integrable
848 end
st └─┘
849
850 /-- The Bochner integral over simple functions in l1 space as a continuous linear map. -/
851 def integral_clm : (α →₁ₛ β) →L[ℝ] β :=
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
852 linear_map.mk_continuous ⟨integral, integral_add, integral_smul⟩
853 1 (λf, le_trans (norm_integral_le_norm _) $ by rw one_mul)
854
855 local notation `Integral` := @integral_clm α _ β _ _ _
856
857 open continuous_linear_map
858
859 lemma norm_Integral_le_one : ∥Integral∥ ≤ 1 :=
860 linear_map.mk_continuous_norm_le _ (zero_le_one) _
861
862 section pos_part
863
864 lemma pos_part_to_simple_func (f : α →₁ₛ ℝ) :
id ┴ ┴
src ┴
typ ┴ ┴
865 ∀ₘ a, f.pos_part.to_simple_func a = f.to_simple_func.pos_part a :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
866 begin
867 have eq : ∀ a, f.to_simple_func.pos_part a = max (f.to_simple_func a) 0 := λa, rfl,
id ┴ ┴
typ ┴ ┴
868 have ae_eq : ∀ₘ a, f.pos_part.to_simple_func a = max (f.to_simple_func a) 0,
id ┴
typ ┴
869 { filter_upwards [to_simple_func_eq_to_fun f.pos_part, pos_part_to_fun (f : α →₁ ℝ),
id ┴
typ ┴
870 to_simple_func_eq_to_fun f],
871 simp only [mem_set_of_eq],
872 assume a h₁ h₂ h₃,
873 rw [h₁, coe_pos_part, h₂, ← h₃] },
st ┴ └┘
874 filter_upwards [ae_eq],
875 simp only [mem_set_of_eq],
876 assume a h,
877 rw [h, eq]
st ┴
878 end
st └─┘
879
880 lemma neg_part_to_simple_func (f : α →₁ₛ ℝ) :
id ┴ ┴
src ┴
typ ┴ ┴
881 ∀ₘ a, f.neg_part.to_simple_func a = f.to_simple_func.neg_part a :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
882 begin
883 rw [simple_func.neg_part, measure_theory.simple_func.neg_part],
884 filter_upwards [pos_part_to_simple_func (-f), neg_to_simple_func f],
885 simp only [mem_set_of_eq],
886 assume a h₁ h₂,
887 rw h₁,
888 show max _ _ = max _ _,
889 rw h₂,
890 refl
891 end
st └─┘
892
893 lemma integral_eq_norm_pos_part_sub (f : α →₁ₛ ℝ) : f.integral = ∥f.pos_part∥ - ∥f.neg_part∥ :=
id ┴ ┴
src ┴
typ ┴ ┴
894 begin
895 -- Convert things in `L¹` to their `simple_func` counterpart
896 have ae_eq₁ : ∀ₘ a, f.to_simple_func.pos_part a = (f.pos_part).to_simple_func.map norm a,
id ┴
typ ┴
897 { filter_upwards [pos_part_to_simple_func f],
898 simp only [mem_set_of_eq],
899 assume a h,
900 rw [simple_func.map_apply, h],
901 conv_lhs { rw [← simple_func.pos_part_map_norm, simple_func.map_apply] } },
st └┘
902 -- Convert things in `L¹` to their `simple_func` counterpart
903 have ae_eq₂ : ∀ₘ a, f.to_simple_func.neg_part a = (f.neg_part).to_simple_func.map norm a,
id ┴
typ ┴
904 { filter_upwards [neg_part_to_simple_func f],
905 simp only [mem_set_of_eq],
906 assume a h,
907 rw [simple_func.map_apply, h],
908 conv_lhs { rw [← simple_func.neg_part_map_norm, simple_func.map_apply] } },
st └┘
909 -- Convert things in `L¹` to their `simple_func` counterpart
910 have ae_eq : ∀ₘ a, f.to_simple_func.pos_part a - f.to_simple_func.neg_part a =
id ┴
typ ┴
911 (f.pos_part).to_simple_func.map norm a - (f.neg_part).to_simple_func.map norm a,
912 { filter_upwards [ae_eq₁, ae_eq₂],
913 simp only [mem_set_of_eq],
914 assume a h₁ h₂,
915 rw [h₁, h₂] },
st ┴ └┘
916 rw [integral, norm_eq_bintegral, norm_eq_bintegral, ← simple_func.bintegral_sub],
917 { show f.to_simple_func.bintegral =
918 ((f.pos_part.to_simple_func).map norm - f.neg_part.to_simple_func.map norm).bintegral,
919 apply simple_func.bintegral_congr f.integrable,
920 { show integrable (f.pos_part.to_simple_func.map norm - f.neg_part.to_simple_func.map norm),
921 refine integrable_of_ae_eq _ _,
922 { exact (f.to_simple_func.pos_part - f.to_simple_func.neg_part) },
st └┘
923 { exact (integrable.max_zero f.integrable).sub f.to_simple_func.pos_part.measurable
924 f.to_simple_func.neg_part.measurable (integrable.max_zero f.integrable.neg) },
st └┘
925 exact ae_eq },
st └┘
926 filter_upwards [ae_eq₁, ae_eq₂],
927 simp only [mem_set_of_eq],
928 assume a h₁ h₂, show _ = _ - _,
929 rw [← h₁, ← h₂],
930 have := f.to_simple_func.pos_part_sub_neg_part,
931 conv_lhs {rw ← this},
932 refl },
st └┘
933 { refine integrable_of_ae_eq (integrable.max_zero f.integrable) ae_eq₁ },
st └┘
934 { refine integrable_of_ae_eq (integrable.max_zero f.integrable.neg) ae_eq₂ }
st └─
935 end
st ──┘
936
937 end pos_part
938
939 end simple_func_integral
940
941 end simple_func
942
943 open simple_func
944
945 variables [normed_space ℝ β] [normed_space ℝ γ] [complete_space β]
id ┴ ┴
src ┴ ┴
typ ┴ ┴
946
947 section integration_in_l1
948
949 local notation `to_l1` := coe_to_l1 α β ℝ
950 local attribute [instance] simple_func.normed_group simple_func.normed_space
951
952 open continuous_linear_map
953
954 /-- The Bochner integral in l1 space as a continuous linear map. -/
955 def integral_clm : (α →₁ β) →L[ℝ] β :=
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
956 integral_clm.extend to_l1 simple_func.dense_range simple_func.uniform_inducing
957
958 /-- The Bochner integral in l1 space -/
959 def integral (f : α →₁ β) : β := (integral_clm).to_fun f
id ┴ ┴ ┴
typ ┴ ┴ ┴
960
961 lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := rfl
id ┴
typ ┴
962
963 @[elim_cast] lemma integral_coe_eq_integral (f : α →₁ₛ β) :
id ┴ ┴
typ ┴ ┴
doc └───────┘
964 integral (f : α →₁ β) = f.integral :=
id ┴ ┴
typ ┴ ┴
965 by { refine uniformly_extend_of_ind _ _ _ _, exact simple_func.integral_clm.uniform_continuous }
st └┘
966
967 variables (α β)
968 @[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 :=
id ┴ ┴
typ ┴ ┴
doc └──┘
969 map_zero integral_clm
970 variables {α β}
971
972 lemma integral_add (f g : α →₁ β) : integral (f + g) = integral f + integral g :=
id ┴ ┴
typ ┴ ┴
973 map_add integral_clm f g
974
975 lemma integral_neg (f : α →₁ β) : integral (-f) = - integral f :=
id ┴ ┴
typ ┴ ┴
976 map_neg integral_clm f
977
978 lemma integral_sub (f g : α →₁ β) : integral (f - g) = integral f - integral g :=
id ┴ ┴
typ ┴ ┴
979 map_sub integral_clm f g
980
981 lemma integral_smul (r : ℝ) (f : α →₁ β) : integral (r • f) = r • integral f :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
982 map_smul r integral_clm f
id ┴
typ ┴
983
984 local notation `Integral` := @integral_clm α _ β _ _ _ _
985 local notation `sIntegral` := @simple_func.integral_clm α _ β _ _ _
986
987 lemma norm_Integral_le_one : ∥Integral∥ ≤ 1 :=
988 calc ∥Integral∥ ≤ 1 * ∥sIntegral∥ :
989 op_norm_extend_le _ _ _ $ λs, by {rw one_mul, refl}
st └┘
990 ... = ∥sIntegral∥ : one_mul _
991 ... ≤ 1 : norm_Integral_le_one
992
993 lemma norm_integral_le (f : α →₁ β) : ∥integral f∥ ≤ ∥f∥ :=
id ┴ ┴
typ ┴ ┴
994 calc ∥integral f∥ = ∥Integral f∥ : rfl
995 ... ≤ ∥Integral∥ * ∥f∥ : le_op_norm _ _
996 ... ≤ 1 * ∥f∥ : mul_le_mul_of_nonneg_right norm_Integral_le_one $ norm_nonneg _
997 ... = ∥f∥ : one_mul _
998
999 section pos_part
1000
1001 lemma integral_eq_norm_pos_part_sub (f : α →₁ ℝ) : integral f = ∥pos_part f∥ - ∥neg_part f∥ :=
id ┴ ┴
src ┴
typ ┴ ┴
1002 begin
1003 -- Use `is_closed_property` and `is_closed_eq`
1004 refine @is_closed_property _ _ _ (coe : (α →₁ₛ ℝ) → (α →₁ ℝ))
1005 (λ f : α →₁ ℝ, integral f = ∥pos_part f∥ - ∥neg_part f∥)
1006 l1.simple_func.dense_range (is_closed_eq _ _) _ f,
1007 { exact cont _ },
st └┘
1008 { refine continuous.sub (continuous_norm.comp l1.continuous_pos_part)
1009 (continuous_norm.comp l1.continuous_neg_part) },
st └┘
1010 -- Show that the property holds for all simple functions in the `L¹` space.
1011 { assume s,
1012 norm_cast,
1013 rw [← simple_func.norm_eq, ← simple_func.norm_eq],
1014 exact simple_func.integral_eq_norm_pos_part_sub _}
st └─
1015 end
st ──┘
1016
1017 end pos_part
1018
1019 end integration_in_l1
1020
1021 end l1
1022
1023 variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [complete_space β]
id └┘ └──┘ └┘ ┴
src └┘ └──┘ └┘ ┴
typ └┘ └──┘ └┘ ┴
doc └┘ └──┘ └┘
1024 [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ]
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘
1025
1026 /-- The Bochner integral -/
1027 def integral (f : α → β) : β :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
1028 if hf : measurable f ∧ integrable f
id ┴ ┴
typ ┴ ┴
1029 then (l1.of_fun f hf.1 hf.2).integral
id ┴
typ ┴
1030 else 0
1031
1032 notation `∫` binders `, ` r:(scoped f, integral f) := r
1033
1034 section properties
1035
1036 open continuous_linear_map measure_theory.simple_func
1037
1038 variables {f g : α → β}
1039
1040 lemma integral_eq (f : α → β) (h₁ : measurable f) (h₂ : integrable f) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1041 (∫ a, f a) = (l1.of_fun f h₁ h₂).integral :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1042 dif_pos ⟨h₁, h₂⟩
1043
1044 lemma integral_undef (h : ¬ (measurable f ∧ integrable f)) : (∫ a, f a) = 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1045 dif_neg h
1046
1047 lemma integral_non_integrable (h : ¬ integrable f) : (∫ a, f a) = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
1048 integral_undef $ not_and_of_not_right _ h
1049
1050 lemma integral_non_measurable (h : ¬ measurable f) : (∫ a, f a) = 0 :=
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
1051 integral_undef $ not_and_of_not_left _ h
1052
1053 variables (α β)
1054 @[simp] lemma integral_zero : (∫ a:α, (0:β)) = 0 :=
id ┴ ┴
typ ┴ ┴
doc └──┘
1055 by rw [integral_eq, l1.of_fun_zero, l1.integral_zero]
st ┴
1056
1057 variables {α β}
1058
1059 lemma integral_add
1060 (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1061 (∫ a, f a + g a) = (∫ a, f a) + (∫ a, g a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1062 by rw [integral_eq, integral_eq f hfm hfi, integral_eq g hgm hgi, l1.of_fun_add, l1.integral_add]
id ┴ ┴
typ ┴ ┴
st ┴
1063
1064 lemma integral_neg (f : α → β) : (∫ a, -f a) = - (∫ a, f a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1065 begin
1066 by_cases hf : measurable f ∧ integrable f,
1067 { rw [integral_eq f hf.1 hf.2, integral_eq (λa, - f a) hf.1.neg hf.2.neg, l1.of_fun_neg,
id ┴ ┴ ┴
typ ┴ ┴ ┴
1068 l1.integral_neg] },
st ┴ └┘
1069 { have hf' : ¬(measurable (λa, -f a) ∧ integrable (λa, -f a)),
id ┴ ┴ ┴
typ ┴ ┴ ┴
1070 { rwa [measurable_neg_iff, integrable_neg_iff] },
st └┘
1071 rw [integral_undef hf, integral_undef hf', neg_zero] }
st ┴ └─
1072 end
st ──┘
1073
1074 lemma integral_sub
1075 (hfm : measurable f) (hfi : integrable f) (hgm : measurable g) (hgi : integrable g) :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1076 (∫ a, f a - g a) = (∫ a, f a) - (∫ a, g a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1077 by simp only [sub_eq_add_neg, integral_neg, integral_add, measurable_neg_iff, integrable_neg_iff, *]
1078
1079 lemma integral_smul (r : ℝ) (f : α → β) : (∫ a, r • (f a)) = r • (∫ a, f a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1080 begin
1081 by_cases hf : measurable f ∧ integrable f,
1082 { rw [integral_eq f hf.1 hf.2, integral_eq (λa, r • (f a)), l1.of_fun_smul, l1.integral_smul] },
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st ┴ └┘
1083 { by_cases hr : r = 0,
id ┴
typ ┴
1084 { simp only [hr, measure_theory.integral_zero, zero_smul] },
st └┘
1085 have hf' : ¬(measurable (λa, r • f a) ∧ integrable (λa, r • f a)),
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1086 { rwa [← measurable_smul_iff hr f, ← integrable_smul_iff hr f] at hf },
id ┴ ┴
typ ┴ ┴
st └┘
1087 rw [integral_undef hf, integral_undef hf', smul_zero] }
st ┴ └─
1088 end
st ──┘
1089
1090 lemma integral_mul_left (r : ℝ) (f : α → ℝ) : (∫ a, r * (f a)) = r * (∫ a, f a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1091 integral_smul r f
id ┴ ┴
typ ┴ ┴
1092
1093 lemma integral_mul_right (r : ℝ) (f : α → ℝ) : (∫ a, (f a) * r) = (∫ a, f a) * r :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1094 by { simp only [mul_comm], exact integral_mul_left r f }
id ┴ ┴
typ ┴ ┴
st └┘
1095
1096 lemma integral_div (r : ℝ) (f : α → ℝ) : (∫ a, (f a) / r) = (∫ a, f a) / r :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1097 integral_mul_right r⁻¹ f
id ┴ ┴
typ ┴ ┴
1098
1099 lemma integral_congr_ae (hfm : measurable f) (hgm : measurable g) (h : ∀ₘ a, f a = g a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1100 (∫ a, f a) = (∫ a, g a) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1101 begin
1102 by_cases hfi : integrable f,
1103 { have hgi : integrable g := integrable_of_ae_eq hfi h,
id ┴
typ ┴
1104 rw [integral_eq f hfm hfi, integral_eq g hgm hgi, (l1.of_fun_eq_of_fun f g hfm hfi hgm hgi).2 h] },
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
st ┴ └┘
1105 { have hgi : ¬ integrable g, { rw integrable_congr_ae h at hfi, exact hfi },
id ┴
typ ┴
st └┘
1106 rw [integral_non_integrable hfi, integral_non_integrable hgi] },
st ┴ └┘
1107 end
st └─┘
1108
1109 lemma norm_integral_le_lintegral_norm (f : α → β) :
id ┴ ┴
typ ┴ ┴
1110 ∥(∫ a, f a)∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) :=
id ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
src ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
doc ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
1111 begin
1112 by_cases hf : measurable f ∧ integrable f,
1113 { rw [integral_eq f hf.1 hf.2, ← l1.norm_of_fun_eq_lintegral_norm f hf.1 hf.2],
id ┴ ┴
typ ┴ ┴
1114 exact l1.norm_integral_le _ },
st └┘
1115 { rw [integral_undef hf, _root_.norm_zero],
1116 exact to_real_nonneg }
st └─
1117 end
st ──┘
1118
1119 /-- Lebesgue dominated convergence theorem provides sufficient conditions under which almost
1120 everywhere convergence of a sequence of functions implies the convergence of their integrals. -/
1121 theorem tendsto_integral_of_dominated_convergence {F : ℕ → α → β} {f : α → β} (bound : α → ℝ)
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1122 (F_measurable : ∀ n, measurable (F n))
id ┴ ┴ ┴
typ ┴ ┴ ┴
1123 (f_measurable : measurable f)
id ┴
typ ┴
1124 (bound_integrable : integrable bound)
id └─┘ ┴
typ └─┘ ┴
1125 (h_bound : ∀ n, ∀ₘ a, ∥F n a∥ ≤ bound a)
id ┴ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴ ┴ └───┘ ┴
1126 (h_lim : ∀ₘ a, tendsto (λ n, F n a) at_top (𝓝 (f a))) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1127 tendsto (λn, ∫ a, F n a) at_top (𝓝 $ (∫ a, f a)) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1128 begin
1129 /- To show `(∫ a, F n a) --> (∫ f)`, suffices to show `∥∫ a, F n a - ∫ f∥ --> 0` -/
1130 rw tendsto_iff_norm_tendsto_zero,
1131 /- But `0 ≤ ∥∫ a, F n a - ∫ f∥ = ∥∫ a, (F n a - f a) ∥ ≤ ∫ a, ∥F n a - f a∥, and thus we apply the
1132 sandwich theorem and prove that `∫ a, ∥F n a - f a∥ --> 0` -/
1133 have zero_tendsto_zero : tendsto (λn:ℕ, (0 : ℝ)) at_top (𝓝 0) := tendsto_const_nhds,
1134 have lintegral_norm_tendsto_zero :
1135 tendsto (λn, ennreal.to_real $ ∫⁻ a, ennreal.of_real ∥F n a - f a∥) at_top (𝓝 0) :=
id ┴ └─────────────┘ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────────────┘
typ ┴ └─────────────┘ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
1136 tendsto.comp (tendsto_to_real (zero_ne_top))
1137 (tendsto_lintegral_norm_of_dominated_convergence
1138 F_measurable f_measurable bound_integrable h_bound h_lim),
1139 -- Use the sandwich theorem
1140 refine tendsto_of_tendsto_of_tendsto_of_le_of_le zero_tendsto_zero lintegral_norm_tendsto_zero _ _,
1141 -- Show `0 ≤ ∥∫ a, F n a - ∫ f∥` for all `n`
1142 { simp only [filter.eventually_at_top, norm_nonneg, forall_true_iff, exists_const] },
st └┘
1143 -- Show `∥∫ a, F n a - ∫ f∥ ≤ ∫ a, ∥F n a - f a∥` for all `n`
1144 { simp only [filter.eventually_at_top],
1145 use 0,
1146 assume n hn,
1147 have h₁ : integrable (F n) := integrable_of_integrable_bound bound_integrable (h_bound _),
id ┴ ┴
typ ┴ ┴
1148 have h₂ : integrable f := integrable_of_dominated_convergence bound_integrable h_bound h_lim,
id ┴
typ ┴
1149 rw ← integral_sub (F_measurable _) h₁ f_measurable h₂,
1150 exact norm_integral_le_lintegral_norm _ }
st └─
1151 end
st ──┘
1152
1153 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
1154 lemma tendsto_integral_filter_of_dominated_convergence {ι} {l : filter ι}
id └┘ ┴
src └┘
typ └┘ ┴
1155 {F : ι → α → β} {f : α → β} (bound : α → ℝ)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1156 (hl_cb : l.has_countable_basis)
id ┴
typ ┴
1157 (hF_meas : ∀ᶠ n in l, measurable (F n))
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1158 (f_measurable : measurable f)
id ┴
typ ┴
1159 (h_bound : ∀ᶠ n in l, ∀ₘ a, ∥F n a∥ ≤ bound a)
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
1160 (bound_integrable : integrable bound)
id ┴ └┘
typ ┴ └┘
1161 (h_lim : ∀ₘ a, tendsto (λ n, F n a) l (𝓝 (f a))) :
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1162 tendsto (λn, ∫ a, F n a) l (𝓝 $ (∫ a, f a)) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1163 begin
1164 rw hl_cb.tendsto_iff_seq_tendsto,
1165 { intros x xl,
1166 have hxl, { rw tendsto_at_top' at xl, exact xl },
st └┘
1167 have h := inter_mem_sets hF_meas h_bound,
1168 replace h := hxl _ h,
1169 rcases h with ⟨k, h⟩,
1170 rw ← tendsto_add_at_top_iff_nat k,
id ┴
typ ┴
1171 refine tendsto_integral_of_dominated_convergence _ _ _ _ _ _,
1172 { exact bound },
id └───┘
typ └───┘
st └┘
1173 { intro, refine (h _ _).1, exact nat.le_add_left _ _ },
st └┘
1174 { assumption },
st └┘
1175 { assumption },
st └┘
1176 { intro, refine (h _ _).2, exact nat.le_add_left _ _ },
st └┘
1177 { filter_upwards [h_lim],
1178 simp only [mem_set_of_eq],
1179 assume a h_lim,
1180 apply @tendsto.comp _ _ _ (λn, x (n + k)) (λn, F n a),
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1181 { assumption },
st └┘
1182 rw tendsto_add_at_top_iff_nat,
1183 assumption } },
st └──┘
1184 end
st └─┘
1185
1186 /-- The Bochner integral of a real-valued function `f : α → ℝ` is the difference between the
1187 integral of the positive part of `f` and the integral of the negative part of `f`. -/
1188 lemma integral_eq_lintegral_max_sub_lintegral_min {f : α → ℝ}
id ┴ ┴
src ┴
typ ┴ ┴
1189 (hfm : measurable f) (hfi : integrable f) : (∫ a, f a) =
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1190 ennreal.to_real (∫⁻ a, ennreal.of_real $ max (f a) 0) -
id ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴
doc ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘
1191 ennreal.to_real (∫⁻ a, ennreal.of_real $ - min (f a) 0) :=
id └─┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
src └─┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
typ └─┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
doc └─┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
1192 let f₁ : α →₁ ℝ := l1.of_fun f hfm hfi in
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
1193 -- Go to the `L¹` space
1194 have eq₁ : ennreal.to_real (∫⁻ a, ennreal.of_real $ max (f a) 0) = ∥l1.pos_part f₁∥ :=
id └┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
typ └┘ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
1195 begin
1196 rw l1.norm_eq_norm_to_fun,
1197 congr' 1,
1198 apply lintegral_congr_ae,
1199 filter_upwards [l1.pos_part_to_fun f₁, l1.to_fun_of_fun f hfm hfi],
id ┴
typ ┴
1200 simp only [mem_set_of_eq],
1201 assume a h₁ h₂,
1202 rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
1203 exact le_max_right _ _
1204 end,
st └─┘
1205 -- Go to the `L¹` space
1206 have eq₂ : ennreal.to_real (∫⁻ a, ennreal.of_real $ -min (f a) 0) = ∥l1.neg_part f₁∥ :=
id └─────────────┘ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
1207 begin
1208 rw l1.norm_eq_norm_to_fun,
1209 congr' 1,
1210 apply lintegral_congr_ae,
1211 filter_upwards [l1.neg_part_to_fun_eq_min f₁, l1.to_fun_of_fun f hfm hfi],
id ┴
typ ┴
1212 simp only [mem_set_of_eq],
1213 assume a h₁ h₂,
1214 rw [h₁, h₂, real.norm_eq_abs, abs_of_nonneg],
1215 rw [min_eq_neg_max_neg_neg, _root_.neg_neg, neg_zero],
1216 exact le_max_right _ _
1217 end,
st └─┘
1218 begin
1219 rw [eq₁, eq₂, integral, dif_pos],
1220 exact l1.integral_eq_norm_pos_part_sub _,
1221 { exact ⟨hfm, hfi⟩ }
st └─
1222 end
st ──┘
1223
1224 lemma integral_eq_lintegral_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) (hfm : measurable f) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
1225 (∫ a, f a) = ennreal.to_real (∫⁻ a, ennreal.of_real $ f a) :=
id ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
src ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘
typ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
doc ┴ └┘ └┘ └┘ ┴ └┘ └┘ └┘
1226 begin
1227 by_cases hfi : integrable f,
1228 { rw integral_eq_lintegral_max_sub_lintegral_min hfm hfi,
1229 have h_min : (∫⁻ a, ennreal.of_real (-min (f a) 0)) = 0,
id ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ └─────────────┘ ┴
doc └─────────────┘
1230 { rw lintegral_eq_zero_iff,
1231 { filter_upwards [hf],
1232 simp only [mem_set_of_eq],
1233 assume a h,
1234 simp only [min_eq_right h, neg_zero, ennreal.of_real_zero] },
st └┘
1235 { refine measurable_of_real.comp
1236 ((measurable.neg measurable_id).comp $ measurable.min hfm measurable_const) } },
st └──┘
1237 have h_max : (∫⁻ a, ennreal.of_real (max (f a) 0)) = (∫⁻ a, ennreal.of_real $ f a),
id ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
1238 { apply lintegral_congr_ae,
1239 filter_upwards [hf],
1240 simp only [mem_set_of_eq],
1241 assume a h,
1242 rw max_eq_left h },
st └┘
1243 rw [h_min, h_max, zero_to_real, _root_.sub_zero] },
st ┴ └┘
1244 { rw integral_non_integrable hfi,
1245 rw [integrable_iff_norm, lt_top_iff_ne_top, ne.def, not_not] at hfi,
1246 have : (∫⁻ (a : α), ennreal.of_real (f a)) = (∫⁻ a, ennreal.of_real ∥f a∥),
id ┴ ┴ └─────────────┘ ┴
src └─────────────┘
typ ┴ ┴ └─────────────┘ ┴
doc └─────────────┘
1247 { apply lintegral_congr_ae,
1248 filter_upwards [hf],
1249 simp only [mem_set_of_eq],
1250 assume a h,
1251 rw [real.norm_eq_abs, abs_of_nonneg h] },
st ┴ └┘
1252 rw [this, hfi], refl }
st └─
1253 end
st ──┘
1254
1255 lemma integral_nonneg_of_nonneg_ae {f : α → ℝ} (hf : ∀ₘ a, 0 ≤ f a) : 0 ≤ (∫ a, f a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1256 begin
1257 by_cases hfm : measurable f,
1258 { rw integral_eq_lintegral_of_nonneg_ae hf hfm, exact to_real_nonneg },
st └┘
1259 { rw integral_non_measurable hfm }
st └─
1260 end
st ──┘
1261
1262 lemma integral_nonpos_of_nonpos_ae {f : α → ℝ} (hf : ∀ₘ a, f a ≤ 0) : (∫ a, f a) ≤ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1263 begin
1264 have hf : ∀ₘ a, 0 ≤ (-f) a,
id ┴ ┴
typ ┴ ┴
1265 { filter_upwards [hf], simp only [mem_set_of_eq], assume a h, rwa [pi.neg_apply, neg_nonneg] },
st └┘
1266 have : 0 ≤ (∫ a, -f a) := integral_nonneg_of_nonneg_ae hf,
id ┴ ┴
typ ┴ ┴
1267 rwa [integral_neg, neg_nonneg] at this,
1268 end
st └─┘
1269
1270 lemma integral_le_integral_ae {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f)
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
1271 (hgm : measurable g) (hgi : integrable g) (h : ∀ₘ a, f a ≤ g a) : (∫ a, f a) ≤ (∫ a, g a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1272 le_of_sub_nonneg
1273 begin
1274 rw ← integral_sub hgm hgi hfm hfi,
1275 apply integral_nonneg_of_nonneg_ae,
1276 filter_upwards [h],
1277 simp only [mem_set_of_eq],
1278 assume a,
1279 exact sub_nonneg_of_le
1280 end
st └─┘
1281
1282 lemma integral_le_integral {f g : α → ℝ} (hfm : measurable f) (hfi : integrable f)
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
1283 (hgm : measurable g) (hgi : integrable g) (h : ∀ a, f a ≤ g a) : (∫ a, f a) ≤ (∫ a, g a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1284 integral_le_integral_ae hfm hfi hgm hgi $ univ_mem_sets' h
1285
1286 lemma norm_integral_le_integral_norm (f : α → β) : ∥(∫ a, f a)∥ ≤ ∫ a, ∥f a∥ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1287 have le_ae : ∀ₘ (a : α), 0 ≤ ∥f a∥ := by filter_upwards [] λa, norm_nonneg _,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
1288 classical.by_cases
1289 ( λh : measurable f,
id ┴
typ ┴
1290 calc ∥(∫ a, f a)∥ ≤ ennreal.to_real (∫⁻ a, ennreal.of_real ∥f a∥) : norm_integral_le_lintegral_norm _
id ┴ ┴ ┴ └─────────────┘ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────────────┘
typ ┴ ┴ ┴ └─────────────┘ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
1291 ... = ∫ a, ∥f a∥ : (integral_eq_lintegral_of_nonneg_ae le_ae $ measurable.norm h).symm )
id ┴ ┴ ┴
typ ┴ ┴ ┴
1292 ( λh : ¬measurable f,
id ┴
typ ┴
1293 begin
1294 rw [integral_non_measurable h, _root_.norm_zero],
1295 exact integral_nonneg_of_nonneg_ae le_ae
1296 end )
st └─┘
1297
1298 lemma integral_finset_sum {ι} (s : finset ι) {f : ι → α → β}
id └┘ └┘ ┴ ┴ ┴
src └┘ └┘
typ └┘ └┘ ┴ ┴ ┴
doc └┘ └┘
1299 (hfm : ∀ i, measurable (f i)) (hfi : ∀ i, integrable (f i)) :
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
1300 (∫ a, s.sum (λ i, f i a)) = s.sum (λ i, ∫ a, f i a) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
1301 begin
1302 refine finset.induction_on s _ _,
1303 { simp only [integral_zero, finset.sum_empty] },
st └┘
1304 { assume i s his ih,
1305 simp only [his, finset.sum_insert, not_false_iff],
id └───────────┘
src └───────────┘
typ └───────────┘
1306 rw [integral_add (hfm _) (hfi _) (measurable_finset_sum s hfm)
1307 (integrable_finset_sum s hfm hfi), ih] }
id ┴
typ ┴
st ┴ └─
1308 end
st ──┘
1309
1310 end properties
1311
1312 mk_simp_attribute integral_simps "Simp set for integral rules."
1313
1314 attribute [integral_simps] integral_neg integral_smul l1.integral_add l1.integral_sub
doc └────────────┘
1315 l1.integral_smul l1.integral_neg
1316
1317 attribute [irreducible] integral l1.integral
src └─────────┘
doc └─────────┘
1318
1319 end measure_theory